
Conferences in DBLP
(itp) 2010 (conf/itp/2010)
A Formally Verified OS Kernel. Now What? [Citation Graph (, )][DBLP]
Proof Assistants as Teaching Assistants: A View from the Trenches. [Citation Graph (, )][DBLP]
A Certified Denotational Abstract Interpreter. [Citation Graph (, )][DBLP]
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. [Citation Graph (, )][DBLP]
A New Foundation for Nominal Isabelle. [Citation Graph (, )][DBLP]
(Nominal) Unification by Recursive Descent with Triangular Substitutions. [Citation Graph (, )][DBLP]
A Formal Proof of a Necessary and Sufficient Condition for DeadlockFree Adaptive Networks. [Citation Graph (, )][DBLP]
Extending Coq with Imperative Features and Its Application to SAT Verification. [Citation Graph (, )][DBLP]
A Tactic Language for Declarative Proofs. [Citation Graph (, )][DBLP]
Programming Language Techniques for Cryptographic Proofs. [Citation Graph (, )][DBLP]
Nitpick: A Counterexample Generator for HigherOrder Logic Based on a Relational Model Finder. [Citation Graph (, )][DBLP]
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. [Citation Graph (, )][DBLP]
An Efficient Coq Tactic for Deciding Kleene Algebras. [Citation Graph (, )][DBLP]
Fast LCFStyle Proof Reconstruction for Z3. [Citation Graph (, )][DBLP]
The Optimal Fixed Point Combinator. [Citation Graph (, )][DBLP]
Formal Study of Plane Delaunay Triangulation. [Citation Graph (, )][DBLP]
Reasoning with HigherOrder Abstract Syntax and Contexts: A Comparison. [Citation Graph (, )][DBLP]
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. [Citation Graph (, )][DBLP]
Automated MachineChecked Hybrid System Safety Proofs. [Citation Graph (, )][DBLP]
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. [Citation Graph (, )][DBLP]
CaseAnalysis for Rippling and Inductive Proof. [Citation Graph (, )][DBLP]
Importing HOL Light into Coq. [Citation Graph (, )][DBLP]
A Mechanized Translation from HigherOrder Logic to Set Theory. [Citation Graph (, )][DBLP]
The Isabelle Collections Framework. [Citation Graph (, )][DBLP]
Interactive Termination Proofs Using Termination Cores. [Citation Graph (, )][DBLP]
A Framework for Formal Verification of Compiler Optimizations. [Citation Graph (, )][DBLP]
On the Formalization of the Lebesgue Integration Theory in HOL. [Citation Graph (, )][DBLP]
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. [Citation Graph (, )][DBLP]
Equations: A Dependent PatternMatching Compiler. [Citation Graph (, )][DBLP]
A Mechanically Verified AIGtoBDD Conversion Algorithm. [Citation Graph (, )][DBLP]
Inductive Consequences in the Calculus of Constructions. [Citation Graph (, )][DBLP]
Validating QBF Invalidity in HOL4. [Citation Graph (, )][DBLP]
HigherOrder Abstract Syntax in Isabelle/HOL. [Citation Graph (, )][DBLP]
Separation Logic Adapted for Proofs by Rewriting. [Citation Graph (, )][DBLP]
Developing the Algebraic Hierarchy with Type Classes in Coq. [Citation Graph (, )][DBLP]
