scientific article; zbMATH DE number 512782

MaRDI QIDQ4281475zbMATH OpenFDO

Authors Bart Jacobs, Tom Melham

Publication date 10 March 1994

zbMATH Keywords

dependent type theoryhigher order logicHOL theorem-proving system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• A mechanized translation from higher-order logic to set theory
• scientific article; zbMATH DE number 65533
• Optimized encodings of fragments of type theory in first order logic
• Translating a Dependently-Typed Logic to First-Order Logic

Cited in

(14)

• On the adequacy of representing higher order intuitionistic logic as a pure type system
• Translating a Dependently-Typed Logic to First-Order Logic
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• First-Order Logic with Dependent Types
• scientific article; zbMATH DE number 67454 (Why is no real title available?)
• Optimized encodings of fragments of type theory in first-order logic
• Some logical and syntactical observations concerning the first-order dependent type system λP
• scientific article; zbMATH DE number 6744295 (Why is no real title available?)
• A mechanized translation from higher-order logic to set theory
• Translating SUMO-K to Higher-Order Set Theory
• Importing mathematics from HOL into Nuprl
• A shallow embedding of pure type systems into first-order logic
• Dependently typed higher-order logic
• The seven virtues of simple type theory

Describes a project that uses

Uses Software

• HOL

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