Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

DOI10.1016/j.ic.2009.09.003zbMath1186.68102MaRDI QIDQ964000

Dominic P. Mulligan, Murdoch James Gabbay

Publication date: 14 April 2010

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2009.09.003

zbMATH Keywords

typing; beta-reduction; alpha-conversion; lambda-calculus reduction; proof-term

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Uses Software

• ML
• HOL
• Automath
• ALF
• FreshOCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Lectures on the Curry-Howard isomorphism
• The lambda-context calculus (extended version)
• Unification under a mixed prefix
• The foundation of a generic theorem prover
• Nominal unification
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• Nominal rewriting
• Implementing Nominal Unification
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
• One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
• One-and-a-halfth-order Logic
• Curry-Style Types for Nominal Terms
• A Formal Calculus for Informal Equality with Binding
• Computer Science Logic
• Logic Programming
• Adapting Proofs-as-Programs
• Parallel reductions in \(\lambda\)-calculus
• A calculus of lambda calculus contexts
• A typed context calculus