scientific article; zbMATH DE number 7285579

MaRDI QIDQ5140267

No author found.

Publication date: 15 December 2020

Full work available at URL: https://arxiv.org/abs/1803.10143

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

higher-order logicstrong normalizationtyped lambda calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• The foundation of a generic theorem prover
• A symmetric lambda calculus for classical program extraction
• On theories with a combinatorial definition of 'equivalence'
• The duality of computation
• The formal system λδ
• The Structural λ-Calculus
• PAL⁺: a lambda-free logical framework
• Formulae-as-types for an involutive negation
• Explicit substitutions
• Intensional interpretations of functionals of finite type I
• Typed $\lambda$-calculi with one binder
• A formulation of the simple theory of types