A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

DOI10.1016/S0747-7171(85)80040-7zbMath0591.68036OpenAlexW2042219295MaRDI QIDQ1075050

Gérard Huet, Thierry Coquand

Publication date: 1985

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(85)80040-7

zbMATH Keywords

typed lambda calculustheorem-provingfunctional programming languagescomputer-aided proof-checkingcomputer-aided synthesis of provably correct computer programsde Bruijn's Automath languagesGirard's second-order typeshigher-order intuitionistic logicMartin-Löf's intuitionistic type theory

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Intuitionistic mathematics (03F55) Combinatory logic and lambda calculus (03B40) Bibliographies for mathematics in general (00A15) Proof theory and constructive mathematics (03Fxx)

Related Items (2)

Insight in discrete geometry and computational content of a discrete model of the continuum ⋮ A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis

Uses Software

• ML
• Automath
• NQTHM
• LCF
• Cambridge LCF

Cites Work

• Combinatory logic. With two sections by William Craig.
• Algebra of proofs
• Constructions, proofs and the meaning of logical constants
• Propositions and specifications of programs in Martin-Löf's type theory
• Programs as proofs: A synopsis
• Verifying the unification algorithm in LCF
• Foundation of logic programming based on inductive definition
• The undecidability of the second-order unification problem
• The lambda calculus, its syntax and semantics
• A unification algorithm for typed \(\overline\lambda\)-calculus
• LCF considered as a programming language
• A theory of type polymorphism in programming
• Intuitionistic propositional logic is polynomial-space complete
• The typed lambda-calculus is not elementary recursive
• Definitional interpreters for higher-order programming languages
• Edinburgh LCF. A mechanized logic of computation
• Writing programs that construct proofs
• A transfinite type theory with type variables
• A proof of cut-elimination theorem in simple type-theory
• Combinators, \(\lambda\)-terms and proof theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• The Expressiveness of Simple and Second-Order Type Structures
• A While-rule in Martin-Lof's Theory of Types
• Proving Theorems about LISP Functions
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Resolution in type theory
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic
• Completeness in the theory of types
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction