Entity usage

This page lists pages that use the given entity (e.g. Q42). The list is sorted by descending page ID, so that newer pages are listed first.

Showing below up to 50 results in range #1 to #50.

Developing the Algebraic Hierarchy with Type Classes in Coq: Label: en
Separation Logic Adapted for Proofs by Rewriting: Label: en
Higher-Order Abstract Syntax in Isabelle/HOL: Label: en
Validating QBF Invalidity in HOL4: Label: en
Inductive Consequences in the Calculus of Constructions: Label: en
A Mechanically Verified AIG-to-BDD Conversion Algorithm: Label: en
Equations: A Dependent Pattern-Matching Compiler: Label: en
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem: Label: en
On the Formalization of the Lebesgue Integration Theory in HOL: Label: en
A Framework for Formal Verification of Compiler Optimizations: Label: en
Interactive Termination Proofs Using Termination Cores: Label: en
The Isabelle Collections Framework: Label: en
A Mechanized Translation from Higher-Order Logic to Set Theory: Label: en
Importing HOL Light into Coq: Label: en
Case-Analysis for Rippling and Inductive Proof: Label: en
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study: Label: en
Automated Machine-Checked Hybrid System Safety Proofs: Label: en
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture: Label: en
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison: Label: en
Formal Study of Plane Delaunay Triangulation: Label: en
The Optimal Fixed Point Combinator: Label: en
Fast LCF-Style Proof Reconstruction for Z3: Label: en
An Efficient Coq Tactic for Deciding Kleene Algebras: Label: en
Formal Proof of a Wave Equation Resolution Scheme: The Method Error: Label: en
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder: Label: en
Programming Language Techniques for Cryptographic Proofs: Label: en
A Tactic Language for Declarative Proofs: Label: en
Extending Coq with Imperative Features and Its Application to SAT Verification: Label: en
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks: Label: en
(Nominal) Unification by Recursive Descent with Triangular Substitutions: Label: en
A New Foundation for Nominal Isabelle: Label: en
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure: Label: en
A Certified Denotational Abstract Interpreter: Label: en
Steps towards Verified Implementations of HOL Light: Label: en
Towards Certifying Network Calculus: Label: en
Implementing Hash-Consed Structures in Coq: Label: en
Stateless Higher-Order Logic with Quantified Types: Label: en
The Picard Algorithm for Ordinary Differential Equations in Coq: Label: en
Square Root and Division Elimination in PVS: Label: en
Communicating Formal Proofs: The Case of Flyspeck: Label: en
A Parallelized Theorem Prover for a Logic with Parallel Execution: Label: en
Shared-Memory Multiprocessing for Interactive Theorem Proving: Label: en
Automatically Generated Infrastructure for De Bruijn Syntaxes: Label: en
Subformula Linking as an Interaction Method: Label: en
Program Extraction from Nested Definitions: Label: en
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques: Label: en
Handcrafted Inversions Made Operational on Operational Semantics: Label: en
Adjustable References: Label: en
Practical Probability: Applying pGCL to Lattice Scheduling: Label: en
Formal Reasoning about Classified Markov Chains in HOL: Label: en