|
|
Conferences in DBLP
- Mauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, Wolfgang J. Paul
On the Correctness of Operating System Kernels. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:1-16 [Conf]
- Andrew M. Pitts
Alpha-Structural Recursion and Induction. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:17-34 [Conf]
- Hasan Amjad
Shallow Lazy Proofs. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:35-49 [Conf]
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
Mechanized Metatheory for the Masses: The PoplMark Challenge. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:50-65 [Conf]
- Christoph Benzmüller, Chad E. Brown
A Structured Set of Higher-Order Problems. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:66-81 [Conf]
- Néstor Cataño
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:82-97 [Conf]
- Benjamin Grégoire, Assia Mahboubi
Proving Equalities in a Commutative Ring Done Right in Coq. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:98-113 [Conf]
- John Harrison
A HOL Theory of Euclidean Space. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:114-129 [Conf]
- Peter V. Homeier
A Design Structure for Higher Order Quotients. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:130-146 [Conf]
- Brian Huffman, John Matthews, Peter White
Axiomatic Constructor Classes in Isabelle/HOLCF. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:147-162 [Conf]
- Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith
Meta Reasoning in ACL2. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:163-178 [Conf]
- Claude Marché, Christine Paulin-Mohring
Reasoning About Java Programs with Aliasing and Frame Conditions. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:179-194 [Conf]
- César Muñoz, David Lester
Real Number Calculations and Theorem Proving. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:195-210 [Conf]
- David A. Naumann
Verifying a Secure Information Flow Analyzer. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:211-226 [Conf]
- Steven Obua
Proving Bounds for Real Linear Programs in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:227-244 [Conf]
- Russell O'Connor
Essential Incompleteness of Arithmetic Verified by Coq. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:245-260 [Conf]
- Veronika Ortner, Norbert Schirmer
Verification of BDD Normalization. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:261-277 [Conf]
- Nicolas Oury
Extensionality in the Calculus of Constructions. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:278-293 [Conf]
- Tom Ridge, James Margetson
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:294-309 [Conf]
- Julien Schmaltz, Dominique Borrione
A Generic Network on Chip Model. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:310-325 [Conf]
- Diana Toma, Dominique Borrione
Formal Verification of a SHA-1 Circuit Core Using ACL2. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:326-341 [Conf]
- Thomas Tuerk, Klaus Schneider
From PSL to LTL: A Formal Validation in HOL. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:342-357 [Conf]
- Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:358-372 [Conf]
- J. Strother Moore, Qiang Zhang
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:373-384 [Conf]
- Tobias Nipkow, Lawrence C. Paulson
Proof Pearl: Defining Functions over Finite Sets. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:385-396 [Conf]
- Michael Norrish, Konrad Slind
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. [Citation Graph (0, 0)][DBLP]
TPHOLs, 2005, pp:397-408 [Conf]
|
