Conferences in DBLP
Tobias Nipkow Verified Lexical Analysis. [Citation Graph (0, 0)][DBLP ] Conf ] Joakim von Wright Extending Window Inference. [Citation Graph (0, 0)][DBLP ] Conf ] Marco Benini , Sara Kalvala , Dirk Nowotka Program Abstraction in a Higher-Order Logic Framework. [Citation Graph (0, 0)][DBLP ] Conf ] Karthikeyan Bhargavan , Carl A. Gunter , Elsa L. Gunter , Michael Jackson , Davor Obradovic , Pamela Zave The Village Telephone System: A Case Study in Formal Software Engineering. [Citation Graph (0, 0)][DBLP ] Conf ] Richard J. Boulton Generating Embeddings from Denotational Descriptions. [Citation Graph (0, 0)][DBLP ] Conf ] Richard J. Boulton , Konrad Slind , Alan Bundy , Michael J. C. Gordon An Interface between Clam and HOL. [Citation Graph (0, 0)][DBLP ] Conf ] James L. Caldwell Classical Propositional Decidability via Nuprl Proof Extraction. [Citation Graph (0, 0)][DBLP ] Conf ] W. O. David Griffioen , Marieke Huisman A Comparison of PVS and Isabelle/HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Elsa L. Gunter Adding External Decision Procedures to HOL90 Securely. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison Formalizing Basic First Order Model Theory. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison Formalizing Dijkstra. [Citation Graph (0, 0)][DBLP ] Conf ] Peter V. Homeier , David F. Martin Mechanical Verification of Total Correctness through Diversion Verification Conditions. [Citation Graph (0, 0)][DBLP ] Conf ] Douglas J. Howe A Type Annotation Scheme for Nuprl. [Citation Graph (0, 0)][DBLP ] Conf ] Paul B. Jackson Verifying a Garbage Collection Algorithm. [Citation Graph (0, 0)][DBLP ] Conf ] Karsten Konrad HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. [Citation Graph (0, 0)][DBLP ] Conf ] Chuck Liang Free Variables and Subexpressions in Higher-Order Meta Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Maxim Lifantsev , Leo Bachmair An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. [Citation Graph (0, 0)][DBLP ] Conf ] Anna Mikhajlova , Joakim von Wright Proving Isomorphism of First-Order Logic Proof Systems in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Roderick Moten Exploiting Parallelism in Interactive Theorem Provers. [Citation Graph (0, 0)][DBLP ] Conf ] Olaf Müller I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle. [Citation Graph (0, 0)][DBLP ] Conf ] Wolfgang Naraschewski , Markus Wenzel Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Naren Narasimhan , Ranga Vemuri On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System. [Citation Graph (0, 0)][DBLP ] Conf ] David Nowak , Jean-René Beauvais , Jean-Pierre Talpin Co-inductive Axiomatization of a Synchronous Language. [Citation Graph (0, 0)][DBLP ] Conf ] François Puitg , Jean-François Dufourd Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. [Citation Graph (0, 0)][DBLP ] Conf ] Rimvydas Ruksenas , Joakim von Wright A Tool for Data Refinement. [Citation Graph (0, 0)][DBLP ] Conf ] Hajime Sawamura , Daisaku Asanuma Mechanizing Relevant Logics with HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Friedrich W. von Henke , Stephan Pfab , Holger Pfeifer , Harald Rueß Case Studies in Meta-Level Theorem Proving. [Citation Graph (0, 0)][DBLP ] Conf ] Mitsuharu Yamamoto , Koichi Takahashi , Masami Hagiya , Shin-ya Nishizaki , Tetsuo Tamai Formalization of Graph Search Algorithms and Its Applications. [Citation Graph (0, 0)][DBLP ] Conf ] 