Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477669zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow, Lawrence C. 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

Mathematics Subject Classification ID

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

Cited in

(10)

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

Describes a project that uses

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)