Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMATH Open1152.68529OpenAlexW2484880499MaRDI QIDQ5477669FDOQ5477669

Lawrence C. Paulson, Tobias Nipkow

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

Recommendations

• Set theory for verification. II: Induction and recursion
• Theory and applications of inverting functions as folds
• Inductively defined functions in functional programming languages
• A tutorial on the universality and expressiveness of fold
• scientific article; zbMATH DE number 2185686

Mathematics Subject Classification ID

Cited In (10)

• Flyspeck II: The basic linear programs
• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
• Formal power series
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)
• Formal SOS-Proofs for the Lambda-Calculus
• Automatic refinement to efficient data structures: a comparison of two approaches

Uses Software

• Isabelle/HOL

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 Q5477669)