Interpretation of Locales in Isabelle: Theories and Proof Contexts
From MaRDI portal
Publication:5756774
DOI10.1007/11812289_4zbMath1188.68258OpenAlexW1532290481MaRDI QIDQ5756774
Publication date: 5 September 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11812289_4
Related Items
Automating change of representation for proofs in discrete mathematics (extended version) ⋮ Balancing the load. Leveraging a semantics stack for systems verification ⋮ Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 ⋮ Let’s Get Physical: Models and Methods for Real-World Security Protocols ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ A formally verified proof of the central limit theorem ⋮ Unnamed Item ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Unnamed Item ⋮ A mechanized proof of the basic perturbation lemma ⋮ The Isabelle Framework ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ Linear quantifier elimination ⋮ Change Management for Heterogeneous Development Graphs ⋮ From LCF to Isabelle/HOL ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ 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 ⋮ Local Theory Specifications in Isabelle/Isar ⋮ Formalizing the Edmonds-Karp Algorithm ⋮ Logic-Free Reasoning in Isabelle/Isar ⋮ Locales: a module system for mathematical theories
Uses Software
