Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477669
DOI10.1007/11541868zbMath1152.68529OpenAlexW2484880499MaRDI QIDQ5477669
Tobias Nipkow, Lawrence Charles Paulson
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
Related Items
A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Flyspeck II: The basic linear programs, Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Formal power series, A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL, Formal SOS-Proofs for the Lambda-Calculus, Effect polymorphism in higher-order logic (proof pearl), Effect polymorphism in higher-order logic (proof pearl), Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
Uses Software
