Isabelle

swMATH454WikidataQ460340MaRDI QIDQ13212

No author found.

Described by source

• The Isabelle Framework

Related Items (only showing first 100 items - show all)

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Strong eventual consistency of the collaborative editing framework WOOT ⋮ Verified bytecode verifiers. ⋮ A unified framework for the computational comparison of adaptive mesh refinement strategies for all-quadrilateral and all-hexahedral meshes: locally adaptive multigrid methods versus h-adaptive methods ⋮ A modular first formalisation of combinatorial design theory ⋮ Beautiful formalizations in Isabelle/Naproche ⋮ Formalizing axiomatic systems for propositional logic in Isabelle/HOL ⋮ CICM'21 systems entries ⋮ An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ The undecidability of proof search when equality is a logical connective ⋮ Nominal logic, a first order theory of names and binding ⋮ The role of entropy in guiding a connection prover ⋮ Automated verification of the parallel Bellman-Ford algorithm ⋮ A logic for Miranda, revisited ⋮ Levels of truth ⋮ Set theory for verification. II: Induction and recursion ⋮ Shedding new light on the foundations of abstract argumentation: modularization and weak admissibility ⋮ Mechanised assessment of complex natural-language arguments using expressive logic combinations ⋮ Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL ⋮ Verifying randomised social choice ⋮ Certification of nonclausal connection tableaux proofs ⋮ Some general results about proof normalization ⋮ N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker ⋮ On the limits of refinement-testing for model-checking CSP ⋮ Mathematical morphology on bipolar fuzzy sets: general algebraic framework ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Formal reasoning under cached address translation ⋮ Exploring the structure of an algebra text with locales ⋮ Relational characterisations of paths ⋮ Formal proof of a machine closed theorem in Coq ⋮ Special issue: Formal proof ⋮ A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L ⋮ Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L ⋮ OrclassWeb: a tool based on the classification methodology ORCLASS from verbal decision analysis framework ⋮ A framework for formal dynamic dependability analysis using HOL theorem proving ⋮ Induction with generalization in superposition reasoning ⋮ Simple dataset for proof method recommendation in Isabelle/HOL ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ From types to sets by local type definition in higher-order logic ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Verifying OpenJDK's sort method for generic collections ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ Certifying proofs in the first-order theory of rewriting ⋮ Refinement to imperative HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Fundamentals of logic and computation. With practical automated reasoning and verification ⋮ Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ A graph library for Isabelle ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ From LCF to Isabelle/HOL ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ An algebraic framework for minimum spanning tree problems ⋮ Modal Kleene algebra applied to program correctness ⋮ An algebra of synchronous atomic steps ⋮ Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings ⋮ Mechanisation of the AKS algorithm ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ A Coq formalisation of SQL's execution engines ⋮ A formalization of the LLL basis reduction algorithm ⋮ Fast machine words in Isabelle/HOL ⋮ Towards verified handwritten calculational proofs (short paper) ⋮ Program verification in the presence of cached address translation ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Relational data across mathematical libraries ⋮ MMTTeX: connecting content and narration-oriented document formats ⋮ Diagram combinators in MMT ⋮ Affine systems of ODEs in Isabelle/HOL for hybrid-program verification ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ Using the Isabelle ontology framework -- linking the formal with the informal ⋮ Isabelle import infrastructure for the Mizar Mathematical Library ⋮ Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL ⋮ Automatically finding theory morphisms for knowledge management ⋮ Goal-oriented conjecturing for Isabelle/HOL ⋮ Verifying asymptotic time complexity of imperative programs in Isabelle ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Priority inheritance protocol proved correct ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ Random belief system dynamics in complex networks under time-varying logic constraints ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ Experiences from exporting major proof assistant libraries ⋮ Dependent types for program termination verification ⋮ Logic-independent proof search in logical frameworks (short paper) ⋮ Structuring metatheory on inductive definitions ⋮ A formalization of Dedekind domains and class groups of global fields ⋮ Theorem proving as constraint solving with coherent logic ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ A formalization of the Smith normal form in higher-order logic ⋮ Planning proofs of equations in CCS ⋮ \textsc{Prawf}: an interactive proof system for program extraction ⋮ A formalization and proof checker for Isabelle's metalogic

This page was built for software: Isabelle