Isabelle
From MaRDI portal
Software:13212
swMATH454WikidataQ460340 ScholiaQ460340MaRDI QIDQ13212FDOQ13212
Author name not available (Why is that?)
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
- Animating the Formalised Semantics of a Java-Like Language
- Three Chapters of Measure Theory in Isabelle/HOL
- 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?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated theorem proving for special functions: the next phase
- Isabelle as Document-Oriented Proof Assistant
- Higher-order rewrite systems and their confluence
- A formally verified proof of the prime number theorem
- Ribbon Proofs for Separation Logic
- 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
- Types for Proofs and Programs
- Types for Proofs and Programs
- Sledgehammer: Judgement Day
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Structured Induction Proofs in Isabelle/Isar
- Algebras for Program Correctness in Isabelle/HOL
- 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
- A Proof Theoretic Interpretation of Model Theoretic Hiding
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Title not available (Why is that?)
- An algebraic framework for minimum spanning tree problems
- Certifying algorithms
- 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
- Preface
- Automated Reasoning
- A meta linear logical framework
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Logic Based Program Synthesis and Transformation
- A Verified Runtime for a Verified Theorem Prover
- From Tarski to Hilbert
- Automated Reasoning in Higher-Order Regular Algebra
- Unifying Lazy and Strict Computations
- On the limits of refinement-testing for model-checking CSP
- Shortening of Proof Length is Elusive for Theorem Provers
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms
- 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
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- Title not available (Why is that?)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- The Flow of ODEs
- Verification of dynamic bisimulation theorems in Coq
- Mechanizing coinduction and corecursion in higher-order logic
- An approach to automatic deductive synthesis of functional programs
- Title not available (Why is that?)
- The refinement calculus of reactive systems
- Programming Combinations of Deduction and BDD-based Symbolic Calculation
- Bytecode verification by model checking
- Title not available (Why is that?)
- A UTP approach for rTiMo
- Mechanized metatheory revisited
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
This page was built for software: Isabelle