scientific article
From MaRDI portal
Publication:3856127
zbMath0422.68045MaRDI QIDQ3856127
Publication date: 1980
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
normalizationintuitionistic predicate logictyped lambda-calculusmechanical verificationChurch-Rosser propertyarithmetical systemsautomath
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Artificial intelligence (68T99) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Combinatory logic and lambda calculus (03B40)
Related Items
Structured theory presentations and logic representations ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ On confluence for weakly normalizing systems ⋮ A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ On the syntax of Martin-Löf's type theories ⋮ A higher-order calculus and theory abstraction ⋮ The calculus of constructions ⋮ Subtyping + extensionality: Confluence of βηtop reduction in F≤ ⋮ Logic representation in LF ⋮ Checking algorithms for Pure Type Systems ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Type checking with universes ⋮ Coquand's calculus of constructions: A mathematical foundation for a proof development system ⋮ Definition and basic properties of the Deva meta-calculus ⋮ Automath and Pure Type Systems ⋮ On the proof theory of Coquand's calculus of constructions ⋮ Telescopic mappings in typed lambda calculus ⋮ Unnamed Item ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
