scientific article; zbMATH DE number 2085164

MaRDI QIDQ4736387zbMATH OpenFDO

Authors Stefan Berghofer, Tobias Nipkow

Publication date 9 August 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2277/22770024.htm

zbMATH Keywords

theorem prover Isabelle/HOL

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1424012
• Term rewriting and beyond -- theorem proving in Isabelle
• Partial Recursive Functions in Higher-Order Logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Partial and nested recursive function definitions in higher-order logic

Cited in

(27)

• Adapting functional programs to higher order logic
• Introduction to ``Milestones in interactive theorem proving
• Verified bytecode verifiers.
• Verified bytecode verification and type-certifying compilation
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
• Isabelle's metalogic: formalization and proof checker
• A formalization and proof checker for Isabelle's metalogic
• From LCF to Isabelle/HOL
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Proof Pearl: regular expression equivalence and relation algebra
• Code-carrying theories
• Teaching semantics with a proof assistant: no more LSD trip proofs
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Turning Inductive into Equational Specifications
• Formalizing the Logic-Automaton Connection
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• The Isabelle Framework
• Memoization
• Verified Root-Balanced Trees
• Extracting functional programs from Coq, in Coq
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• A formal analysis of capacity scaling algorithms for minimum cost flows
• Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
• Priority Search Trees
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Proof synthesis and reflection for linear arithmetic
• Partial and nested recursive function definitions in higher-order logic

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication:

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