Concrete Semantics

DOI10.1007/978-3-319-10542-0zbMath1410.68004OpenAlexW4250850800MaRDI QIDQ2926333

Tobias Nipkow, Gerwin Klein

Publication date: 23 October 2014

Full work available at URL: https://doi.org/10.1007/978-3-319-10542-0

Mathematics Subject Classification ID

Related Items (62)

Soundness and completeness proofs by coinductive methods ⋮ ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Semantic representation of general topology in the Wolfram language ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Quotients of Bounded Natural Functors ⋮ Verified Approximation Algorithms ⋮ Verification of Closest Pair of Points Algorithms ⋮ Mining the Archive of Formal Proofs ⋮ Verified Root-Balanced Trees ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Verified iptables firewall analysis and verification ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Consistent Foundation for Isabelle/HOL ⋮ A Linear First-Order Functional Intermediate Language for Verified Compilers ⋮ A formalized general theory of syntax with bindings ⋮ αCheck: A mechanized metatheory model checker ⋮ Unifying splitting ⋮ A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL ⋮ Binary Generalized PCP for Two Periodic Morphisms is Decidable in Polynomial Time ⋮ Targeted configuration of an SMT solver ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Unnamed Item ⋮ Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types ⋮ Amortized complexity verified ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Flag-based big-step semantics ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ On the semantics of polychronous polytimed specifications ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ An algebraic framework for minimum spanning tree problems ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol ⋮ A formal proof of the expressiveness of deep learning ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Verified analysis of random binary tree structures ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A comprehensive framework for saturation theorem proving ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Translating Scala Programs to Isabelle/HOL ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A unifying splitting framework ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ Automatic Functional Correctness Proofs for Functional Search Trees ⋮ A comprehensive framework for saturation theorem proving ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Verifying graph programs with monadic second-order logic

Uses Software

• Isabelle/HOL

This page was built for publication: Concrete Semantics