Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL

DOI10.1007/978-3-642-03359-9_22zbMath1252.68260OpenAlexW1871548459MaRDI QIDQ3183537

Andreas Lochbihler

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_22

Mathematics Subject Classification ID

Related Items

A verified algorithm enumerating event structures, A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Animating the Formalised Semantics of a Java-Like Language, FinFuns

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Nominal Isabelle
• Jinja Threads
• AVL trees
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• Constructive Type Classes in Isabelle
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Partial Recursive Functions in Higher-Order Logic
• Theorem Proving in Higher Order Logics