constructive type theory
Recently Published Documents


TOTAL DOCUMENTS

68
(FIVE YEARS 6)

H-INDEX

9
(FIVE YEARS 1)

Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.


2021 ◽  
Vol 31 (1) ◽  
pp. 112-151
Author(s):  
Yannick Forster ◽  
Dominik Kirst ◽  
Dominik Wehr

Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak K̋nig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.


2019 ◽  
Vol 29 (4) ◽  
pp. 469-486 ◽  
Author(s):  
Liron Cohen ◽  
Robert L Constable

Abstract In this article we define pure intuitionistic Ancestral Logic ( iAL ), extending pure intuitionistic First-Order Logic ( iFOL ). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for the transitive closure, TC . We derive this operator from the natural type theoretic definition of TC using intersection. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable.


2019 ◽  
Vol 66 (2) ◽  
pp. 1-35
Author(s):  
Vincent Rahli ◽  
Mark Bickford ◽  
Liron Cohen ◽  
Robert L. Constable

2018 ◽  
Vol 28 (9) ◽  
pp. 1578-1605
Author(s):  
FURIO HONSELL ◽  
LUIGI LIQUORI ◽  
PETAR MAKSIMOVIĆ ◽  
IVAN SCAGNETTO

We present two extensions of theLFconstructive type theory featuring monadiclocks. A lock is a monadic type construct that captures the effect of anexternal call to an oracle. Such calls are the basic tool forplugging-inand gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in thecanonical styledeveloped by the ‘CMU School.’ The first system,CLLF𝒫, is the canonical version of the systemLLF𝒫, presented earlier by the authors. The second system,CLLF𝒫?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms ofCLLF𝒫andCLLF𝒫?permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standardLFencodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.


Sign in / Sign up

Export Citation Format

Share Document