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
• 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