The following pages link to Isabelle (Q13212):
Displaying 50 items.
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Classification of finite fields with applications (Q2323448) (← links)
- An Isabelle/HOL formalisation of Green's theorem (Q2323451) (← links)
- Formalization of geometric algebra in HOL Light (Q2323452) (← links)
- A verified compiler from Isabelle/HOL to CakeML (Q2324018) (← links)
- Hierarchical specification and verification of architectural design patterns (Q2324187) (← links)
- Efficient verification of imperative programs using auto2 (Q2324204) (← links)
- Model-theoretic conservative extension for definitional theories (Q2333319) (← links)
- First steps towards a formalization of forcing (Q2333671) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Infinite executions of lazy and strict computations (Q2347906) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Using Isabelle/HOL to verify first-order relativity theory (Q2351148) (← links)
- Locales: a module system for mathematical theories (Q2352487) (← links)
- Proving divide and conquer complexities in Isabelle/HOL (Q2362108) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Presentation and manipulation of Mizar properties in an Isabelle object logic (Q2364678) (← links)
- A verified algorithm enumerating event structures (Q2364684) (← links)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- Classification of alignments between concepts of formal mathematical systems (Q2364703) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- Morphism axioms (Q2402279) (← links)
- Satisfiability modulo bounded checking (Q2405244) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- A survey on temporal logics for specifying and verifying real-time systems (Q2418645) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Formal reasoning about finite-state discrete-time Markov chains in HOL (Q2434565) (← links)
- Decomposition of conflict as a distribution on hypotheses in the framework on belief functions (Q2447774) (← links)
- An approach to automatic deductive synthesis of functional programs (Q2457802) (← links)
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book (Q2462639) (← links)
- On the mechanization of the proof of Hessenberg's theorem in coherent logic (Q2471743) (← links)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- Rewriting conversions implemented with continuations (Q2655323) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
- Better than optimal mean-variance portfolio policy in multi-period asset-liability management problem (Q2661546) (← links)
- Binary intersection formalized (Q2662679) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- The refinement calculus of reactive systems (Q2672236) (← links)
- Post-quantum verification of Fujisaki-Okamoto (Q2692346) (← links)
- Automated reasoning for probabilistic sequential programs with theorem proving (Q2695373) (← links)
- Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle (Q2703745) (← links)
- Theorem proving in infinitesimal geometry (Q2720298) (← links)
