Isabelle

swMATH454WikidataQ460340 ScholiaQ460340MaRDI QIDQ13212FDOQ13212

Author name not available (Why is that?)

Described by source

• The Isabelle Framework

Cited In (only showing first 100 items - show all)

• A logical framework combining model and proof theory
• Graphical reasoning in compact closed categories for quantum computation
• Conjecture synthesis for inductive theories
• Dynamic asset allocation in a mean-variance framework
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Title not available (Why is that?)
• Natural deduction for non-classical logics
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• Relational and Kleene-Algebraic Methods in Computer Science
• A first order logic of effects
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Title not available (Why is that?)
• Formal power series
• Mathematical Knowledge Management
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated theorem proving for special functions: the next phase
• Higher-order rewrite systems and their confluence
• A formally verified proof of the prime number theorem
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Monotonicity inference for higher-order formulas
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• A proof theoretic interpretation of model theoretic hiding
• Towards logical frameworks in the heterogeneous tool set Hets
• Types for Proofs and Programs
• Types for Proofs and Programs
• Shortening of proof length is elusive for theorem provers
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Structured Induction Proofs in Isabelle/Isar
• Mechanical Theorem Proving in Tarski’s Geometry
• Psi-calculi in Isabelle
• Experiments with proof plans for induction
• Computer supported mathematics with \(\Omega\)MEGA
• Fractional variational integrators for fractional variational problems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An inductive approach to strand spaces
• Proof Pearl: regular expression equivalence and relation algebra
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• Sledgehammer: judgement day
• A verified runtime for a verified theorem prover
• Isabelle as document-oriented proof assistant
• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Ribbon proofs for separation logic
• Formalization and execution of linear algebra: from theorems to algorithms
• Interactive theorem proving from the perspective of Isabelle/Isar
• Unifying lazy and strict computations
• Algebras for program correctness in Isabelle/HOL
• Title not available (Why is that?)
• An algebraic framework for minimum spanning tree problems
• Certifying algorithms
• Proof certificates for algebra and their application to automatic geometry theorem proving
• Shallow confluence of conditional term rewriting systems
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Data compression for proof replay
• Hoare logic for Java in Isabelle/HOL
• Proof automation for functional correctness in separation logic
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• Infinite executions of lazy and strict computations
• Constructive Type Classes in Isabelle
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Automated Reasoning
• A meta linear logical framework
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Animating the formalised semantics of a Java-like language
• Three chapters of measure theory in Isabelle/HOL
• Logic Based Program Synthesis and Transformation
• From Tarski to Hilbert
• Automated Reasoning in Higher-Order Regular Algebra
• On the limits of refinement-testing for model-checking CSP
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Title not available (Why is that?)
• Partizan Games in Isabelle/HOLZF
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Tool-Based Verification of a Relational Vertex Coloring Program
• Confluence by decreasing diagrams -- formalized
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal verification of an executable LTL model checker with partial order reduction
• Title not available (Why is that?)
• Imperative Functional Programming with Isabelle/HOL
• Isabelle formalization of set theoretic structures and set comprehensions
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Towards an awareness-based semantics for security protocol analysis
• Proving linearizability with temporal logic
• Automating Algebraic Specifications of Non-freely Generated Data Types
• Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics
• The use of embeddings to provide a clean separation of term and annotation for higher order rippling
• Proof search and proof check for equational and inductive theorems.

This page was built for software: Isabelle