Code Generation via Higher-Order Rewrite Systems
From MaRDI portal
Publication:3558332
DOI10.1007/978-3-642-12251-4_9zbMath1284.68131OpenAlexW1523874359MaRDI QIDQ3558332
Florian Haftmann, Tobias Nipkow
Publication date: 4 May 2010
Published in: Functional and Logic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-12251-4_9
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE, Proving divide and conquer complexities in Isabelle/HOL, A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Soundness and completeness proofs by coinductive methods, Unnamed Item, Automatic Proof and Disproof in Isabelle/HOL, Formalization and Execution of Linear Algebra: From Theorems to Algorithms, Verified Root-Balanced Trees, Proof Pearl: regular expression equivalence and relation algebra, CoSMed: a confidentiality-verified social media platform, Verified iptables firewall analysis and verification, A verified SAT solver framework with learn, forget, restart, and incrementality, Deriving Comparators and Show Functions in Isabelle/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, VeriMon: a formally verified monitoring tool, Combining higher-order logic with set theory formalizations, Unnamed Item, Verified decision procedures for MSO on words based on derivatives of regular expressions, Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm, Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Friends with Benefits, Comprehending Isabelle/HOL’s Consistency, Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL, Verification and code generation for invariant diagrams in Isabelle, Programming and verifying a declarative first-order prover in Isabelle/HOL, Amortized complexity verified, A verified implementation of the Berlekamp-Zassenhaus factorization algorithm, Reachability, confluence, and termination analysis with state-compatible automata, A framework for developing stand-alone certifiers, Partiality and recursion in interactive theorem provers – an overview, From LCF to Isabelle/HOL, CoCon: a conference management system with formally verified document confidentiality, Efficient verified (UN)SAT certificate checking, A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality, Translating Scala Programs to Isabelle/HOL, Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments, Animating the Formalised Semantics of a Java-Like Language, Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism, Isabelle's metalogic: formalization and proof checker, Certified equational reasoning via ordered completion, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Trustworthy Graph Algorithms (Invited Talk), CoSMed: A Confidentiality-Verified Social Media Platform, Formalizing the Edmonds-Karp Algorithm, Hipster: Integrating Theory Exploration in a Proof Assistant, Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?, A formalization and proof checker for Isabelle's metalogic, Proof pearl: A mechanized proof of GHC's mergesort
Uses Software
