The following pages link to Isabelle/HOL (Q14275):
Displayed 50 items.
- Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22--24, 2010. Revised selected papers (Q645925) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
- Amortized complexity verified (Q670702) (← links)
- Formal verification of an executable LTL model checker with partial order reduction (Q682350) (← links)
- A formalization of metric spaces in HOL Light (Q682381) (← links)
- Linear quantifier elimination (Q707743) (← links)
- Relational bytecode correlations (Q710672) (← links)
- The world's shortest correct exact real arithmetic program? (Q714620) (← links)
- Frame rule for mutually recursive procedures manipulating pointers (Q732009) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Optimising the ProB model checker for B using partial order reduction (Q736463) (← links)
- An operational semantics for object-oriented concepts based on the class hierarchy (Q736789) (← links)
- Test-data generation for control coverage by proof (Q736805) (← links)
- Concerned with the unprivileged: user programs in kernel refinement (Q736848) (← links)
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings (Q739160) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- Analysis of a clock synchronization protocol for wireless sensor networks (Q764293) (← links)
- Two case studies of semantics execution in Maude: CCS and LOTOS (Q816216) (← links)
- Program extraction from normalization proofs (Q817701) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Lyndon words formalized in Isabelle/HOL (Q832940) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- Verification of sequential and concurrent programs (Q837527) (← links)
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm (Q839031) (← links)
- Using La\TeX\ as a semantic markup format (Q841688) (← links)
- Cones and foci: A mechanical framework for protocol verification (Q853730) (← links)
- Mathematical method and proof (Q857692) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Verifying the SET purchase protocols (Q861698) (← links)
- Formal analysis of multiparty contract signing (Q861699) (← links)
- Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Security types preserving compilation (Q865705) (← links)
- Verification of FPGA layout generators in higher-order logic (Q877830) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings (Q955386) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)