Conferences in DBLP
Sten Agerholm Translating Specifications in VDM-SL to PVS. [Citation Graph (0, 0)][DBLP ] Conf ] Sten Agerholm , Ilya Beylin , Peter Dybjer A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. [Citation Graph (0, 0)][DBLP ] Conf ] David A. Basin , Stefan Friedrich Modeling a Hardware Synthesis Methodology in Isabelle. [Citation Graph (0, 0)][DBLP ] Conf ] Paul E. Black , Phillip J. Windley Inference Rules for Programming Languages with Side Effects in Expressions. [Citation Graph (0, 0)][DBLP ] Conf ] Stephen H. Brackin Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. [Citation Graph (0, 0)][DBLP ] Conf ] Holger Busch Proving Liveness of Fair Transition Systems. [Citation Graph (0, 0)][DBLP ] Conf ] Michael J. Butler , Thomas Långbacka Program Derivation Using the Refinement Calculator. [Citation Graph (0, 0)][DBLP ] Conf ] Graham Collins A Proof Tool for Reasoning About Functional Programs. [Citation Graph (0, 0)][DBLP ] Conf ] Solange Coupet-Grimal , Line Jakubiec Coq and Hardware Verification: A Case Study. [Citation Graph (0, 0)][DBLP ] Conf ] Bruno Dutertre Elements of Mathematical Analysis in PVS. [Citation Graph (0, 0)][DBLP ] Conf ] Dirk Eisenbiegler , Christian Blumenröhr , Ramayya Kumar Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Andrew D. Gordon , Thomas F. Melham Five Axioms of Alpha-Conversion. [Citation Graph (0, 0)][DBLP ] Conf ] Michael J. C. Gordon Set Theory, Higher Order Logic or Both? [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison A Mizar Mode for HOL. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison Stålmarck's Algorithm as a HOL Derived Rule. [Citation Graph (0, 0)][DBLP ] Conf ] Mark Heckman , Cui Zhang , Brian R. Becker , Dave Peticolas , Karl N. Levitt , Ronald A. Olsson Towards Applying the Composition Principle to Verify a Microkernel Operating System. [Citation Graph (0, 0)][DBLP ] Conf ] Barbara Heyd , Pierre Crégut A Modular Coding of UNITY in COQ. [Citation Graph (0, 0)][DBLP ] Conf ] Douglas J. Howe Importing Mathematics from HOL into Nuprl. [Citation Graph (0, 0)][DBLP ] Conf ] Kolyang , Thomas Santen , Burkhart Wolff A Structure Preserving Encoding of Z in Isabelle/HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Mats Larsson Improving the Result of High-Level Synthesis Using Interactive Transformational Design. [Citation Graph (0, 0)][DBLP ] Conf ] Linas Laibinis Using Lattice Theory in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Dieter Nazareth , Tobias Nipkow Formal Verification of Algorithm W: The Monomorphic Case. [Citation Graph (0, 0)][DBLP ] Conf ] Cornelia Pusch Verification of Compiler Correctness for the WAM. [Citation Graph (0, 0)][DBLP ] Conf ] Bernhard Reus Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. [Citation Graph (0, 0)][DBLP ] Conf ] Konrad Slind Function Definition in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Alan Smaill , Ian Green Higher-Order Annotated Terms for Proof Search. [Citation Graph (0, 0)][DBLP ] Conf ] Sofiène Tahar , Paul Curzon A Comparison of MDG and HOL for Hardware Verification. [Citation Graph (0, 0)][DBLP ] Conf ] Vincent Zammit A Mechanisation of Computability Theory in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] 