scholarly journals Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

2018 ◽  
Vol 274 ◽  
pp. 11-26 ◽  
Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro
Keyword(s):  
Type Theory ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Generic Structures

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