scholarly journals Plugging-in proof development environments usingLocksinLF

2018 ◽  
Vol 28 (9) ◽  
pp. 1578-1605
Author(s):  
FURIO HONSELL ◽  
LUIGI LIQUORI ◽  
PETAR MAKSIMOVIĆ ◽  
IVAN SCAGNETTO
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Basic Tool ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Canonical Version

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.

scholarly journals On the existence of Stone-Čech compactification

2010 ◽  
Vol 75 (4) ◽  
pp. 1137-1146 ◽  
Author(s):  
Giovanni Curi
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Natural Extension ◽  
Formal System ◽  
Topological Spaces ◽  
Completely Regular ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Constructive Set Theory ◽  
In Virtue Of

Introduction. In 1937 E. Čech and M.H. Stone, independently, introduced the maximal compactification of a completely regular topological space, thereafter called Stone-Čech compactification [8, 23]. In the introduction of [8] the non-constructive character of this result is so described: “It must be emphasized that β(S) [the Stone-Čech compactification of S] may be defined only formally (not constructively) since it exists only in virtue of Zermelo's theorem”.By replacing topological spaces with locales, Banaschewski and Mulvey [4, 5, 6], and Johnstone [14] obtained choice-free intuitionistic proofs of Stone-Čech compactification. Although valid in any topos, these localic constructions rely—essentially, as is to be demonstrated—on highly impredicative principles, and thus cannot be considered as constructive in the sense of the main systems for constructive mathematics, such as Martin-Löf's constructive type theory and Aczel's constructive set theory.In [10] I characterized the locales of which the Stone-Čech compactification can be defined in constructive type theory CTT, and in the formal system CZF+uREA+DC, a natural extension of Aczel's system for constructive set theory CZF by a strengthening of the Regular Extension Axiom REA and the principle of Dependent Choice.

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

2021 ◽  
pp. 1-20
Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Proof Assistant ◽  
First Order ◽  
Constructive Type Theory ◽  
Fundamental Part ◽  
Constructive Type ◽  
Free Variables ◽  
The Church ◽  
Theoretical Results

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.

Recursively Defined Types in Constructive Type Theory

1989 ◽  
pp. 369-410 ◽  
Author(s):  
PRAKASH PANANGADEN ◽  
PAUL MENDLER ◽  
MICHAEL I. SCHWARTZBACH
Keyword(s):  
Type Theory ◽  
Constructive Type Theory ◽  
Constructive Type

Tychonoff's theorem in the framework of formal topologies

1997 ◽  
Vol 62 (4) ◽  
pp. 1315-1332 ◽  
Author(s):  
Sara Negri ◽  
Silvio Valentini
Keyword(s):  
Type Theory ◽  
Constructive Proof ◽  
Topological Product ◽  
Essential Difference ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Definition Of ◽  
The Axiom Of Choice ◽  
Inductive Property ◽  
Formal Topology

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.

scholarly journals Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

2011 ◽  
pp. 609-638 ◽  
Author(s):  
Steve Awodey ◽  
Richard Garner ◽  
Per Martin-Löf ◽  
Vladimir Voevodsky
Keyword(s):  
Type Theory ◽  
Constructive Type Theory ◽  
Constructive Type

The calculus of dependent lambda eliminations

2017 ◽  
Vol 27 ◽  
Author(s):  
AARON STUMP
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Prototype Implementation ◽  
Constructive Type Theory ◽  
Typed Lambda Calculus ◽  
Constructive Type

AbstractModern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.

Sign in / Sign up

Export Citation Format

Share Document