Isabelle/HOL
From MaRDI portal
swMATH1569MaRDI QIDQ14275FDOQ14275
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Cited In (only showing first 100 items - show all)
- Why do the relativistic masses and momenta of faster-than-light particles decrease as their speeds increase?
- A logical framework combining model and proof theory
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Tarski geometry axioms. III
- Two case studies of semantics execution in Maude: CCS and LOTOS
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- The axiomatization of override and update
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- A trusted mechanised JavaSript specification
- Bridging the Gap: Automatic Verified Abstraction of C
- A condensed semantics for qualitative spatial reasoning about oriented straight line segments
- Formal power series
- Algebra of monotonic Boolean transformers
- A decision procedure for linear ``big O equations
- Concurrent dynamic algebra
- Principles of proof scores in CafeOBJ
- Title not available (Why is that?)
- Automated theorem proving for special functions: the next phase
- Combining Decision Procedures by (Model-)Equality Propagation
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Extending a Resolution Prover for Inequalities on Elementary Functions
- A framework for the verification of certifying computations
- Automated Deduction – CADE-20
- Towards MKM in the large: modular representation and scalable software architecture
- Invariant diagrams with data refinement
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- Decreasing diagrams and relative termination
- Monotonicity inference for higher-order formulas
- Towards logical frameworks in the heterogeneous tool set Hets
- A universal machine for biform theory graphs
- A Formal Language for Cryptographic Pseudocode
- Title not available (Why is that?)
- Types for Proofs and Programs
- Using Isabelle/HOL to verify first-order relativity theory
- Formalising the π-Calculus Using Nominal Logic
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Verification of sequential and concurrent programs
- Partial Recursive Functions in Higher-Order Logic
- Towards finding longer proofs
- Behavioral interface specification languages
- Unbounded discrepancy of deterministic random walks on grids
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Title not available (Why is that?)
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- The representational adequacy of Hybrid
- Title not available (Why is that?)
- Verification conditions for source-level imperative programs
- Applications of real number theorem proving in PVS
- An inductive approach to strand spaces
- On theorem prover-based testing
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- E-MaLeS 1.1
- Proof Pearl: regular expression equivalence and relation algebra
- A learning-based fact selector for Isabelle/HOL
- A Perron-Frobenius theorem for deciding matrix growth
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Formal verification of graph grammars using mathematical induction
- Automated Deduction in Geometry
- Verification and code generation for invariant diagrams in Isabelle
- Title not available (Why is that?)
- An algebraic framework for minimum spanning tree problems
- Operating system verification---an overview
- Analysis of a clock synchronization protocol for wireless sensor networks
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Recent advances in program verification through computer algebra
- A two-valued logic for properties of strict functional programs allowing partial functions
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Mathematical Knowledge Management
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Hoare logic for Java in Isabelle/HOL
- Selected papers from the workshops on disproving and the second international workshop on pragmatics of decision procedures (PDPAR 2004), Cork, Ireland, 2004
- Reachability analysis over term rewriting systems
- Proving pointer programs in higher-order logic
- Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings
- The mechanisation of Barendregt-style equational proofs (the residual perspective)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- On the role of formalization in computational mathematics
- Partial and nested recursive function definitions in higher-order logic
- Modeling and verifying graph transformations in proof assistants
- Tools and Algorithms for the Construction and Analysis of Systems
- Mechanically certifying formula-based Noetherian induction reasoning
- Code generation via higher-order rewrite systems
- Animating the formalised semantics of a Java-like language
- Proof pearl: the marriage theorem
- A unifying splitting framework
- Refinements for free!
- Types, bytes, and separation logic
- Reachability, confluence, and termination analysis with state-compatible automata
- Homography in \(\mathbb{R}\mathbb{P}^2\)
- Scalable LCF-style proof translation
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Computer Science Logic
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
- Certified Size-Change Termination
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- A dyadic deontic logic in HOL
- Generalized and formalized uncurrying
- Formal proof of a wave equation resolution scheme: the method error
This page was built for software: Isabelle/HOL
