Partial Recursive Functions in Higher-Order Logic
From MaRDI portal
Publication:3613436
DOI10.1007/11814771_48zbMath1222.68367OpenAlexW1569975162MaRDI QIDQ3613436
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
Related Items
Flyspeck II: The basic linear programs ⋮ Formalizing the Logic-Automaton Connection ⋮ Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL ⋮ A compiled implementation of normalisation by evaluation ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Pattern Matches in HOL: ⋮ Friends with Benefits ⋮ The Isabelle Framework ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ Amortized complexity verified ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Another Look at Function Domains ⋮ Unnamed Item ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Automating Side Conditions in Formalized Partial Functions ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
Uses Software
