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.

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives: Label: en
Coherent and Strongly Discrete Rings in Type Theory: Label: en
A Formal Proof of Square Root and Division Elimination in Embedded Programs: Label: en
Rating Disambiguation Errors: Label: en
Constructive Completeness for Modal Logic with Transitive Closure: Label: en
Compact Proof Certificates for Linear Logic: Label: en
A String of Pearls: Proofs of Fermat’s Little Theorem: Label: en
Proof Pearl: Abella Formalization of λ-Calculus Cube Property: Label: en
Shall We Juggle, Coinductively?: Label: en
Compositional Verification of a Baby Virtual Memory Manager: Label: en
Noninterference for Operating System Kernels: Label: en
Proving Concurrent Noninterference: Label: en
The New Quickcheck for Isabelle: Label: en
Producing Certified Functional Code from Inductive Specifications: Label: en
Mechanized Verification of Computing Dominators for Formalizing Compilers: Label: en
A Formally-Verified Alias Analysis: Label: en
Proof Pearl: The Marriage Theorem: Label: en
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience: Label: en
Coquet: A Coq Library for Verifying Hardware: Label: en
Hardware-Dependent Proofs of Numerical Programs: Label: en
Mechanizing the Metatheory of mini-XQuery: Label: en
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”: Label: en
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL: Label: en
Tactics for Reasoning Modulo AC in Coq: Label: en
Modular SMT Proofs for Fast Reflexive Checking Inside Coq: Label: en
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses: Label: en
A Decision Procedure for Regular Expression Equivalence in Type Theory: Label: en
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars: Label: en
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem: Label: en
Formalization of Wu’s Simple Method in Coq: Label: en
Univalent Semantics of Constructive Type Theories: Label: en
A Proposal for Broad Spectrum Proof Certificates: Label: en
Automated Certification of Implicit Induction Proofs: Label: en
Proof-Carrying Code in a Session-Typed Process Calculus: Label: en
Constructive Formalization of Hybrid Logic with Eventualities: Label: en
A Formal Model and Correctness Proof for an Access Control Policy Framework: Label: en
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties: Label: en
Formalizing Probabilistic Noninterference: Label: en
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax: Label: en
Certifiably Sound Parallelizing Transformations: Label: en
Formalizing the SAFECode Type System: Label: en
Extracting Proofs from Tabled Proof Search: Label: en
Certified Kruskal’s Tree Theorem: Label: en
A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem: Label: en
Refinements for Free!: Label: en
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL: Label: en
Nonfree Datatypes in Isabelle/HOL: Label: en
Certified Parsing of Regular Languages: Label: en
A Constructive Theory of Regular Languages in Coq: Label: en
Aliasing Restrictions of C11 Formalized in Coq: Label: en