Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMath1152.68422OpenAlexW2484880499MaRDI QIDQ5477662

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

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

Related Items (2)

ANF preserves dependent types up to extensional equality ⋮ The compatibility of the minimalist foundation with homotopy type theory

Uses Software

• Nuprl

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