Search results for "TPHOLs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Pertti Kellomäki	A Structural Embedding of Ocsid in PVS.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Natarajan Shankar	Using Decision Procedures with a Higher-Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena	HELM and the Semantic Math-Web.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001	The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability).	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Giampaolo Bella, Lawrence C. Paulson	Mechanical Proofs about a Non-repudiation Protocol.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Louise A. Dennis, Alan Smaill	Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Ana Bove, Venanzio Capretta	Nested General Recursion and Partiality in Type Theory.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre	Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Mario Cáccamo, Glynn Winskel	A Higher-Order Calculus for Categories.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Gertrud Bauer, Markus Wenzel 0001	Calculational Reasoning Revisited (An Isabelle/Isar Experience).	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Bart Jacobs 0001	JavaCard Program Verification.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Matt Fairtlough, Michael Mendler, Xiaochun Cheng	Abstraction and Refinement in Higher Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	David Hemer, Ian J. Hayes, Paul A. Strooper	Refinement Calculus for Logic Programming in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003	Proving Hybrid Protocols Correct.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	R. D. Arthan	An Irrational Construction of R from Z.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	John Harrison 0001	Formal Verification of IA-64 Division Algorithms.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Abdel Mokkedem, Tim Leonard	Formal Verification of the Alpha 21364 Network Protocol.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	M. Randall Holmes	A Strong and Mechanizable Grand Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Jim Grundy	Verified Optimizations for the Intel IA-64 Architecture.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Robert Pollack	Dependently Typed Records for Representing Mathematical Structure.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Robin Milner	Graphical Theories of Interactive Systems: Can a Proof Assistant Help?	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Victor Carreño, César A. Muñoz	Aircraft Trajectory Modeling and Altering Algorithm Verification.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin	Specification and Verification of a Steam-Boiler with Signal-Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF	the steam-boiler problem, theorem proving, synchronous programming
1	Linas Laibinis, Joakim von Wright	Functional Procedures in Higher-Order Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Ewen Denney	A Prototype Proof Translator from HOL to Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Konrad Slind	Another Look at Nested Recursion.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Herman Geuvers, Freek Wiedijk, Jan Zwanenburg	Equational Reasoning via Partial Reflection.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Bruno Barras	Programming and Computing in HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Antonia Balaa, Yves Bertot	Fix-Point Equations for Well-Founded Recursion in Type Theory.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Venanzio Capretta	Recursive Families of Inductive Types.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Bernhard Reus, Tatjana Hein	Towards a Machine-Checked Java Specification Book.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Jason Hickey, Aleksey Nogin	Fast Tactic-Based Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Marieke Huisman, Bart Jacobs 0001	Inheritance in Higher Order Logic: Modeling and Reasoning.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Stefan Berghofer, Tobias Nipkow	Proof Terms for Simply Typed Higher Order Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Mark D. Aagaard, John Harrison 0001 (eds.)	Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Christoph Lüth, Burkhart Wolff	TAS - A Generic Window Inference System.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Hanne Gottliebsen	Transcendental Functions and Continuity Checking in PVS.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Roope Kaivola, Mark D. Aagaard	Divider Circuit Verification with Model Checking and Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Michael J. C. Gordon	Reachability Programming in HOL98 Using BDDs.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Catherine Dubois	Proving ML Type Soundness Within Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic	Routing Information Protocol in HOL/SPIN.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Larry Wos	Appendix: Conjectures Concerning Proof, Design, and Verification.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Larry Wos, Branden Fitelson	Automating the Search for Answers to Open Questions.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Stephan Merz	Weak Alternating Automata in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Pierre Letouzey, Laurent Théry	Formalizing Stålmarck's Algorithm in Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Robert P. Colwell, Bob Brennan	Intel's Formal Verification Experience on the Willamette Development.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Jacques D. Fleuriot	On the Mechanization of Real Analysis in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Martin Hofmann 0001, Francis Tang	Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Paul B. Jackson	Total-Correctness Refinement for Sequential Reactive Systems.	TPHOLs	2000	DBLP DOI BibTeX RDF
1	Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson	Locales - A Sectioning Concept for Isabelle.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Venanzio Capretta	Universal Algebra in Type Theory.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Klaus Schneider 0001, Dirk W. Hoffmann	A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Mark Staples	Representing WP Semantics in Isabelle/ZF.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Don Syme	Three Tactic Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Stefan Berghofer, Markus Wenzel 0001	Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Norbert Völker	Disjoint Sums over Type Classes in HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Olga Caprotti, Arjeh M. Cohen	Connecting Proof Checkers and Computer Algebra Using OpenMath.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Nancy A. Day, Jeffrey J. Joyce	Symbolic Functional Evaluation.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Vincent Zammit	On the Implementation of an Extensible Declarative Proof Language.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Bernd Grobauer, Olaf Müller	From I/O Automata to Timed I/O Automata.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Simon Ambler, Roy L. Crole	Mechanized Operational Semantics via (Co)Induction.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Solange Coupet-Grimal, Line Jakubiec	Hardware Verification Using Co-induction in COQ.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Markus Wenzel 0001	Isar - A Generic Interpretative Approach to Readable Formal Proof Documents.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	John Harrison 0001	A Machine-Checked Theory of Floating Point Arithmetic.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Dominique Bolignano	Formal Methods and Security Evaluation (Invited Talk).	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Thomas Kropf	Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger	Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Holger Pfeifer, Harald Rueß	Polytypic Proof Construction.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	John Matthews	Recursive Function Definition over Coinductive Types.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Thomas Santen	Isomorphisms - A Link Between the Shallow and the Deep.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Haiyan Xiong, Paul Curzon, Sofiène Tahar	Importing MDG Verification Results into HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry (eds.)	Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Joe Hurd	Integrating Gandalf and HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Rimvydas Ruksenas, Joakim von Wright	A Tool for Data Refinement.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	John Harrison 0001	Formalizing Basic First Order Model Theory.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	John Harrison 0001	Formalizing Dijkstra.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai	Formalization of Graph Search Algorithms and Its Applications.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Richard J. Boulton	Generating Embeddings from Denotational Descriptions.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Jim Grundy, Malcolm C. Newey (eds.)	Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Wolfgang Naraschewski, Markus Wenzel 0001	Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	François Puitg, Jean-François Dufourd	Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Hajime Sawamura, Daisaku Asanuma	Mechanizing Relevant Logics with HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Roderick Moten	Exploiting Parallelism in Interactive Theorem Provers.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	James L. Caldwell	Classical Propositional Decidability via Nuprl Proof Extraction.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Paul B. Jackson	Verifying a Garbage Collection Algorithm.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson 0001, Davor Obradovic, Pamela Zave	The Village Telephone System: A Case Study in Formal Software Engineering.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Douglas J. Howe	A Type Annotation Scheme for Nuprl.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	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.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Elsa L. Gunter	Adding External Decision Procedures to HOL90 Securely.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Tobias Nipkow	Verified Lexical Analysis.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Joakim von Wright	Extending Window Inference.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Chuck C. Liang	Free Variables and Subexpressions in Higher-Order Meta Logic.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß	Case Studies in Meta-Level Theorem Proving.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Karsten Konrad	HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Maxim Lifantsev, Leo Bachmair	An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	David Nowak, Jean-René Beauvais, Jean-Pierre Talpin	Co-inductive Axiomatization of a Synchronous Language.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon	An Interface between Clam and HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Peter V. Homeier, David F. Martin	Mechanical Verification of Total Correctness through Diversion Verification Conditions.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Olaf Müller	I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle.	TPHOLs	1998	DBLP DOI BibTeX RDF

Publications at "TPHOLs"( http://dblp.L3S.de/Venues/TPHOLs )