Extensional set equality in the calculus of constructions

DOI10.1093/LOGCOM/11.3.483MaRDI QIDQ2752532zbMATH OpenOpenAlexFDO

Authors Jonathan P. Seldin

Publication date 14 May 2002

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/11.3.483

zbMATH Keywords

typed \(\lambda\)-calculusextensionalityset theorycalculus of constructionstrusted systems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Other set-theoretic hypotheses and axioms (03E65)

Recommendations

• Theorem Proving in Higher Order Logics
• On the proof theory of Coquand's calculus of constructions
• Interpreting HOL in the calculus of constructions
• The calculus of constructions
• scientific article; zbMATH DE number 1746890

Cited in

(8)

• External equality and absolute equality coincide in finite CCS and calculus without summation
• Interpreting HOL in the calculus of constructions
• Variants of the basic calculus of constructions
• Extensional crisis and proving identity
• Type theories from Barendregt's cube for theorem provers
• Set theory in predicate calculus with equality
• Theorem Proving in Higher Order Logics
• Sets in Coq, Coq in Sets

This page was built for publication: Extensional set equality in the calculus of constructions

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