Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477662zbMATH OpenOpenAlexFDO

Authors Nicolas Oury

Publication date 6 July 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• The calculus of constructions
• Extensional set equality in the calculus of constructions
• Inductive consequences in the calculus of constructions
• scientific article; zbMATH DE number 1361477
• Setoid type theory -- a syntactic translation

Cited in

(8)

• Equiconsistency of the minimalist foundation with its classical version
• ANF preserves dependent types up to extensional equality
• scientific article; zbMATH DE number 5316130 (Why is no real title available?)
• A construction of one-point bases in extended lambda calculi
• Exits in the refinement calculus
• Extensional set equality in the calculus of constructions
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• The compatibility of the minimalist foundation with homotopy type theory

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Theorem Proving in Higher Order Logics

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