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 #101 to #150.

ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages: Label: en
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions: Label: en
A Linear First-Order Functional Intermediate Language for Verified Compilers: Label: en
Foundational Property-Based Testing: Label: en
Amortized Complexity Verified: Label: en
Affine Arithmetic and Applications to Real-Number Proving: Label: en
HOCore in Coq: Label: en
Stream Fusion for Isabelle’s Code Generator: Label: en
Refinement to Imperative/HOL: Label: en
A Consistent Foundation for Isabelle/HOL: Label: en
Learning to Parse on Aligned Corpora (Rough Diamond): Label: en
A Verified Enclosure for the Lorenz Attractor (Rough Diamond): Label: en
A Formalized Hierarchy of Probabilistic System Types: Label: en
Improved Tool Support for Machine-Code Decompilation in HOL4: Label: en
Proof-Producing Reflection for HOL: Label: en
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker: Label: en
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation: Label: en
Mechanisation of AKS Algorithm: Part 1 – The Main Theorem: Label: en
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra: Label: en
Validating Dominator Trees for a Fast, Verified Dominance Test: Label: en
A Concrete Memory Model for CompCert: Label: en
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface: Label: en
ROSCoq: Robots Powered by Constructive Reals: Label: en
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory: Label: en
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems: Label: en
Formalization of Shannon’s Theorems in SSReflect-Coq: Label: en
Priority Inheritance Protocol Proved Correct: Label: en
Towards Provably Robust Watermarking: Label: en
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq: Label: en
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm: Label: en
Bag Equivalence via a Proof-Relevant Membership Relation: Label: en
Verifying and Generating WP Transformers for Procedures on Complex Data: Label: en
Abstract Interpretation of Annotated Commands: Label: en
Bridging the Gap: Automatic Verified Abstraction of C: Label: en
A Refinement-Based Approach to Computational Algebra in Coq: Label: en
Construction of Real Algebraic Numbers in Coq: Label: en
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers: Label: en
Abella: A Tutorial: Label: en
A Differential Operator Approach to Equational Differential Invariants: Label: en
Computer-Aided Cryptographic Proofs: Label: en
MetiTarski: Past and Future: Label: en
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL: Label: en
A Language of Patterns for Subterm Selection: Label: en
More SPASS with Isabelle: Label: en
Mechanised Separation Algebra: Label: en
Charge!: Label: en
Using Locales to Define a Rely-Guarantee Temporal Logic: Label: en
A Compact Proof of Decidability for Regular Expression Equivalence: Label: en
Certification of Nontermination Proofs: Label: en
Stop When You Are Almost-Full: Label: en