Interpreting HOL in the calculus of constructions

DOI10.1016/j.jal.2004.02.003zbMath1051.03015OpenAlexW2034899574MaRDI QIDQ1885479

Jonathan P. Seldin

Publication date: 28 October 2004

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2004.02.003

zbMATH Keywords

HOLExtensionalityCalculus of constructionsTheorem-proving

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Uses Software

• ML
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• A Gentzen-style sequent calculus of constructions with expansion rules
• Extensional Set Equality in the Calculus of Constructions
• On lists and other abstract data types in the calculus of constructions
• The Logic of Choice
• Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
• On the proof theory of Coquand's calculus of constructions

This page was built for publication: Interpreting HOL in the calculus of constructions