scientific article; zbMATH DE number 65536

MaRDI QIDQ4012884zbMATH OpenFDO

Authors Lincoln Wallen, David Pym

Publication date 27 September 1992

zbMATH Keywords

cut-eliminationintrinsic well-typingreduction of search spacesubformula propertysystem for proof-search in the \(\lambda\Pi\)- calculusunification

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Recommendations

• A note on the proof theory of the -calculus
• Investigations into proof-search in a system of first-order dependent function types
• scientific article; zbMATH DE number 1390270
• scientific article; zbMATH DE number 1231701
• A focused sequent calculus framework for proof search in pure type systems

Cited in

(21)

• Permutability of proofs in intuitionistic sequent calculi
• Constructive proofs of the range property in lambda calculus
• On the intuitionistic force of classical search
• Proof-search in type-theoretic languages: An introduction
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• A note on the proof theory of the -calculus
• A self-contained provability calculus for \(\varGamma_0\)
• A focused sequent calculus framework for proof search in pure type systems
• A sequent calculus with implicit term representation
• scientific article; zbMATH DE number 1231701 (Why is no real title available?)
• The basis decision problem in λ‐calculus
• On the intuitionistic force of classical search (extended abstract)
• Proof-terms for classical and intuitionistic resolution
• scientific article; zbMATH DE number 1424052 (Why is no real title available?)
• Formal SOS-Proofs for the Lambda-Calculus
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• Automata theoretic account of proof search
• CONCUR 2005 – Concurrency Theory
• Investigations into proof-search in a system of first-order dependent function types
• Representing unification in a logical framework
• Using typed lambda calculus to implement formal systems on a machine

This page was built for publication:

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