Conferences in DBLP
Sten Agerholm Translating Specifications in VDM-SL to PVS. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:1-16 [Conf ] Sten Agerholm , Ilya Beylin , Peter Dybjer A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:17-32 [Conf ] David A. Basin , Stefan Friedrich Modeling a Hardware Synthesis Methodology in Isabelle. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:33-50 [Conf ] Paul E. Black , Phillip J. Windley Inference Rules for Programming Languages with Side Effects in Expressions. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:51-60 [Conf ] Stephen H. Brackin Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:61-76 [Conf ] Holger Busch Proving Liveness of Fair Transition Systems. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:77-92 [Conf ] Michael J. Butler , Thomas Långbacka Program Derivation Using the Refinement Calculator. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:93-108 [Conf ] Graham Collins A Proof Tool for Reasoning About Functional Programs. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:109-124 [Conf ] Solange Coupet-Grimal , Line Jakubiec Coq and Hardware Verification: A Case Study. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:125-139 [Conf ] Bruno Dutertre Elements of Mathematical Analysis in PVS. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:141-156 [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 ] TPHOLs, 1996, pp:157-172 [Conf ] Andrew D. Gordon , Thomas F. Melham Five Axioms of Alpha-Conversion. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:173-190 [Conf ] Michael J. C. Gordon Set Theory, Higher Order Logic or Both? [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:191-201 [Conf ] John Harrison A Mizar Mode for HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:203-220 [Conf ] John Harrison Stålmarck's Algorithm as a HOL Derived Rule. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:221-234 [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 ] TPHOLs, 1996, pp:235-250 [Conf ] Barbara Heyd , Pierre Crégut A Modular Coding of UNITY in COQ. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:251-266 [Conf ] Douglas J. Howe Importing Mathematics from HOL into Nuprl. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:267-281 [Conf ] Kolyang , Thomas Santen , Burkhart Wolff A Structure Preserving Encoding of Z in Isabelle/HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:283-298 [Conf ] Mats Larsson Improving the Result of High-Level Synthesis Using Interactive Transformational Design. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:299-314 [Conf ] Linas Laibinis Using Lattice Theory in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:315-330 [Conf ] Dieter Nazareth , Tobias Nipkow Formal Verification of Algorithm W: The Monomorphic Case. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:331-345 [Conf ] Cornelia Pusch Verification of Compiler Correctness for the WAM. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:347-361 [Conf ] Bernhard Reus Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:365-380 [Conf ] Konrad Slind Function Definition in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:381-397 [Conf ] Alan Smaill , Ian Green Higher-Order Annotated Terms for Proof Search. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:399-413 [Conf ] Sofiène Tahar , Paul Curzon A Comparison of MDG and HOL for Hardware Verification. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:415-430 [Conf ] Vincent Zammit A Mechanisation of Computability Theory in HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:431-446 [Conf ]