Combinators, \(\lambda\)-terms and proof theory
From MaRDI portal
Publication:2556396
zbMath0248.02032MaRDI QIDQ2556396
Publication date: 1972
Published in: Synthese Library (Search for Journal in Brave)
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Proof theory and constructive mathematics (03F99)
Related Items
A characterization of F-complete type assignments, On the implementation of abstract data types by programming language constructs, Unnamed Item, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, Algebra of constructions. I. The word problem for partial algebras, The calculus of constructions, Unnamed Item, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Higher-order rewrite systems and their confluence, Intuitive counterexamples for constructive fallacies, Ein starker Normalisationssatz für die bar-rekursiven Funktionale, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, A sequent calculus for type assignment, Prelogic of logoi, Polymorphic lambda calculus: The Church-Rosser property, Inductive-data-type systems, On the proof theory of Coquand's calculus of constructions, Fully abstract models of typed \(\lambda\)-calculi, Theory of proofs (arithmetic and analysis), A solution to Curry and Hindley's problem on combinatory strong reduction, The semantics of second-order lambda calculus, Typing and computational properties of lambda expressions, Combinatory reduction systems: Introduction and survey, Definition of the semantics of programming language constructs in terms of ?-calculus. I, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
