The following pages link to Isabelle (Q13212):
Displaying 50 items.
- Formal proof of a machine closed theorem in Coq (Q1714805) (← links)
- OrclassWeb: a tool based on the classification methodology ORCLASS from verbal decision analysis framework (Q1717914) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Verifying OpenJDK's sort method for generic collections (Q1725846) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Canonical HybridLF: extending Hybrid with dependent types (Q1744412) (← links)
- Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics (Q1748473) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← links)
- A Coq formalisation of SQL's execution engines (Q1791148) (← links)
- A formalization of the LLL basis reduction algorithm (Q1791154) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- Program verification in the presence of cached address translation (Q1791200) (← links)
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (Q1798665) (← links)
- Using the Isabelle ontology framework -- linking the formal with the informal (Q1798941) (← links)
- Isabelle import infrastructure for the Mizar Mathematical Library (Q1798961) (← links)
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL (Q1798967) (← links)
- Automatically finding theory morphisms for knowledge management (Q1798969) (← links)
- Goal-oriented conjecturing for Isabelle/HOL (Q1798971) (← links)
- Verifying asymptotic time complexity of imperative programs in Isabelle (Q1799114) (← links)
- Dependent types for program termination verification (Q1850960) (← links)
- Structuring metatheory on inductive definitions (Q1854368) (← links)
- Planning proofs of equations in CCS (Q1857269) (← links)
- Verified bytecode verifiers. (Q1874284) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- A logic for Miranda, revisited (Q1903076) (← links)
- Levels of truth (Q1903585) (← links)
- Set theory for verification. II: Induction and recursion (Q1904402) (← links)
- Some general results about proof normalization (Q1931341) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
- On the limits of refinement-testing for model-checking CSP (Q1941896) (← links)
- Mathematical morphology on bipolar fuzzy sets: general algebraic framework (Q1951291) (← links)
- Special issue: Formal proof (Q1961912) (← links)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L (Q1961914) (← links)
- Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L (Q1961917) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- A graph library for Isabelle (Q2018659) (← links)
- A process calculus BigrTiMo of mobile systems and its formal semantics (Q2026376) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Mechanisation of the AKS algorithm (Q2031415) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
