Combinators, \(\lambda\)-terms and proof theory

zbMath0248.02032MaRDI QIDQ2556396

Sören Stenlund

Publication date: 1972

Published in: Synthese Library (Search for Journal in Brave)

Mathematics Subject Classification ID

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 (26)

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

This page was built for publication: Combinators, \(\lambda\)-terms and proof theory