Isabelle

swMATH454WikidataQ460340MaRDI QIDQ13212

No author found.

Described by source

• The Isabelle Framework

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

Isabelle. A generic theorem prover ⋮ A UTP approach for rTiMo ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Interactive theorem proving. Preface of the special issue ⋮ On definitions of constants and types in HOL ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Eisbach: a proof method language for Isabelle ⋮ Towards a trustworthy semantics-based language framework via proof generation ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Lyndon words formalized in Isabelle/HOL ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ Balancing the load. Leveraging a semantics stack for systems verification ⋮ Proof pearl: Mechanizing the textbook proof of Huffman's algorithm ⋮ Aligning concepts across proof assistant libraries ⋮ Interactive theorem proving with temporal logic ⋮ Simplifying proofs in Fitch-style natural deduction systems ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ A proof-centric approach to mathematical assistants ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ Verified iptables firewall analysis and verification ⋮ Hammer for Coq: automation for dependent type theory ⋮ Formalization of the resolution calculus for first-order logic ⋮ A deontic logic reasoning infrastructure ⋮ Verification of FPGA layout generators in higher-order logic ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Higher-order rewrite systems and their confluence ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ A scalable module system ⋮ Towards the Mathematics Software Bus ⋮ A first order logic of effects ⋮ Automated flaw detection in algebraic specifications ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ How to simulate it in Isabelle: towards formal proof for secure multi-party computation ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ Programming and automating mathematics in the Tarski-Kleene hierarchy ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ A formally verified proof of the central limit theorem ⋮ Verified bytecode subroutines ⋮ Bytecode verification by model checking ⋮ Using formal reasoning on a model of tasks for FreeRTOS ⋮ Reasoning about memory layouts ⋮ Fractional variational integrators for fractional variational problems ⋮ Conjecture synthesis for inductive theories ⋮ Monotonicity inference for higher-order formulas ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Fermat, Euler, Wilson -- three case studies in number theory ⋮ Towards verification of cyber-physical systems with UTP and Isabelle/HOL ⋮ Certifying algorithms ⋮ Representing model theory in a type-theoretical logical framework ⋮ An inductive approach to strand spaces ⋮ A mechanized proof of the basic perturbation lemma ⋮ Nominal techniques in Isabelle/HOL ⋮ Verification and code generation for invariant diagrams in Isabelle ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Amortized complexity verified ⋮ The seven virtues of simple type theory ⋮ An introduction to mechanized reasoning ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ Proving linearizability with temporal logic ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ A new approach to abstract syntax with variable binding ⋮ Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ The world's shortest correct exact real arithmetic program? ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ Implementing type systems for the IDE with Xsemantics ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Implementing geometric algebra products with binary trees ⋮ A shape graph logic and a shape system ⋮ A Skeptic's approach to combining HOL and Maple ⋮ Winskel is (almost) right: Towards a mechanized semantics textbook ⋮ Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings ⋮ Proof assistants: history, ideas and future ⋮ Labelled modal logics: Quantifiers ⋮ The calculus of constructions as a framework for proof search with set variable instantiation ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Data compression for proof replay ⋮ Natural deduction for non-classical logics ⋮ Graphical reasoning in compact closed categories for quantum computation ⋮ Program development schemata as derived rules ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ Experimenting with Isabelle in ZF set theory ⋮ Isabelle/HOL. A proof assistant for higher-order logic ⋮ Proof planning for strategy development ⋮ Experiments with proof plans for induction ⋮ Set theory for verification. I: From foundations to functions ⋮ Evaluating general purpose automated theorem proving systems ⋮ The future of logic: foundation-independence

This page was built for software: Isabelle