A sequent calculus for type assignment

DOI10.2307/2272314zbMath0369.02014OpenAlexW1974396457MaRDI QIDQ4147961

Jonathan P. Seldin

Publication date: 1977

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

Full work available at URL: https://doi.org/10.2307/2272314

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof theory and constructive mathematics (03F99)

Related Items (5)

Variants of the basic calculus of constructions ⋮ Annual Meeting of the Association for Symbolic Logic, Los Angeles, 1989 ⋮ Coquand's calculus of constructions: A mathematical foundation for a proof development system ⋮ On the proof theory of Coquand's calculus of constructions ⋮ A sequent calculus formulation of type assignment with equality rules for the λβ-calculus

Cites Work

• Functionals defined by recursion
• Combinatory logic. Vol. II
• Combinators, \(\lambda\)-terms and proof theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Intensional interpretations of functionals of finite type I
• Resolution in type theory
• Unnamed Item
• Unnamed Item

This page was built for publication: A sequent calculus for type assignment