Holes with binding power

DOI10.1007/3-540-39185-1_10MaRDI QIDQ4435469zbMATH OpenFDO

Authors Georgi I. Jojgov

Publication date 12 November 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2646/26460162.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Open proofs and open terms: A basis for interactive logic
• The Abella Interactive Theorem Prover (System Description)
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• Tactics and parameters
• Binding structures as an abstract data type

Cited in

(8)

• The lambda-context calculus (extended version)
• PVS\#: streamlined tacticals for PVS
• One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
• Open proofs and open terms: A basis for interactive logic
• Tactics and parameters
• Two-level lambda-calculus
• Nominal Henkin semantics: simply-typed lambda-calculus models in nominal sets
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

This page was built for publication: Holes with binding power

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4435469)