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

DOI10.1016/J.IC.2009.09.003zbMath1186.68102OpenAlexW2076703601MaRDI 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

typingbeta-reductionalpha-conversionlambda-calculus reductionproof-term

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• ML
• HOL
• Automath
• ALF
• FreshOCaml

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms