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 #51 to #100.

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL: Label: en
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types: Label: en
Formalizing Bounded Increase: Label: en
Mechanical Verification of SAT Refutations with Extended Resolution: Label: en
Pragmatic Quotient Types in Coq: Label: en
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL: Label: en
Kleene Algebra with Tests and Coq Tools for while Programs: Label: en
A Machine-Checked Proof of the Odd Order Theorem: Label: en
Mechanising Turing Machines and Computability Theory in Isabelle/HOL: Label: en
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1: Label: en
Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable: Label: en
Data Refinement in Isabelle/HOL: Label: en
Automatic Data Refinement: Label: en
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation: Label: en
Scalable LCF-Style Proof Translation: Label: en
MaSh: Machine Learning for Sledgehammer: Label: en
Canonical Structures for the Working Coq User: Label: en
Automating Theorem Proving with SMT: Label: en
Mechanised Computability Theory: Label: en
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism: Label: en
A Verified Runtime for a Verified Theorem Prover: Label: en
On the Generation of Positivstellensatz Witnesses in Degenerate Cases: Label: en
Formalization of Entropy Measures in HOL: Label: en
Animating the Formalised Semantics of a Java-Like Language: Label: en
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials: Label: en
Proving Valid Quantified Boolean Formulas in HOL Light: Label: en
Validating QBF Validity in HOL4: Label: en
Termination of Isabelle Functions via Termination of Rewriting: Label: en
Three Chapters of Measure Theory in Isabelle/HOL: Label: en
A Formalization of Polytime Functions: Label: en
Point-Free, Set-Free Concrete Linear Algebra: Label: en
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments: Label: en
Towards Robustness Analysis Using PVS: Label: en
Structural Analysis of Narratives with the Coq Proof Assistant: Label: en
Relational Decomposition: Label: en
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq: Label: en
Logical Formalisation and Analysis of the Mifare Classic Card in PVS: Label: en
Advances in the Formalization of the Odd Order Theorem: Label: en
Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers: Label: en
Composable Discovery Engines for Interactive Theorem Proving: Label: en
Lem: A Lightweight Tool for Heavyweight Semantics: Label: en
LCF-Style Bit-Blasting in HOL4: Label: en
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl): Label: en
seL4 Enforces Integrity: Label: en
Automatic Differentiation in ACL2: Label: en
Pattern Matches in HOL:: Label: en
Formalising Knot Theory in Isabelle/HOL: Label: en
Deriving Comparators and Show Functions in Isabelle/HOL: Label: en
A Mechanized Theory of Regular Trees in Dependent Type Theory: Label: en
Transfinite Constructions in Classical Type Theory: Label: en