scientific article; zbMATH DE number 1420794

MaRDI QIDQ4944858zbMATH OpenFDO

Authors Frank Pfenning, Carsten Schürmann

Publication date 22 March 2000

zbMATH Keywords

dependently typed \(\lambda\)-calculusinteraction of notational definitions with algorithms for testing equality and unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1231700
• Foundations of Software Science and Computational Structures
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Reduction and unification in lambda calculi with a general notion of subtype
• A higher-order unification algorithm for inductive types and dependent types

Cited in

(7)

• Automated techniques for provably safe mobile code.
• Logical approximation for program analysis
• Reducing higher-order theorem proving to a sequence of SAT problems
• A canonical locally named representation of binding
• Redundancy elimination for LF
• scientific article; zbMATH DE number 1231700 (Why is no real title available?)
• Reducing higher-order theorem proving to a sequence of SAT problems

Describes a project that uses

Uses Software

• Coq
• Isabelle
• PVS
• Twelf
• LEGO

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 Q4944858)