Partial Recursive Functions in Higher-Order Logic

DOI10.1007/11814771_48MaRDI QIDQ3613436zbMATH OpenOpenAlexFDO

Authors Alexander Krauss

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814771_48

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20)

Recommendations

• Partial and nested recursive function definitions in higher-order logic
• Partial functions in a total setting
• Partiality and recursion in higher-order logic
• scientific article; zbMATH DE number 2185679
• Termination of Isabelle functions via termination of rewriting

Cited in

(28)

• Flyspeck II: The basic linear programs
• Function definition in higher-order logic
• Pattern matches in HOL: a new representation and improved code generation
• Partiality and recursion in higher-order logic
• Formalizing the Logic-Automaton Connection
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• The Isabelle Framework
• scientific article; zbMATH DE number 2185679 (Why is no real title available?)
• A step-indexing approach to partial functions
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Another look at function domains
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Partiality and recursion in interactive theorem provers -- an overview
• A compiled implementation of normalisation by evaluation
• A two-valued logic for properties of strict functional programs allowing partial functions
• Automating Side Conditions in Formalized Partial Functions
• A Compiled Implementation of Normalization by Evaluation
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• Partial and nested recursive function definitions in higher-order logic
• Amortized complexity verified
• On modal logics of partial recursive functions
• Induction proofs with partial functions
• Friends with benefits. Implementing corecursion in foundational proof assistants

Describes a project that uses

Uses Software

• HOL Light
• Isabelle/ZF
• Isabelle/HOL

This page was built for publication: Partial Recursive Functions in Higher-Order Logic

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