Search results for "TPHOLs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Marco Benini, Sara Kalvala, Dirk Nowotka	Program Abstraction in a Higher-Order Logic Framework.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Anna Mikhajlova, Joakim von Wright	Proving Isomorphism of First-Order Logic Proof Systems in HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Albert John Camilleri	A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Bruno Dutertre, Steve A. Schneider	Using a PVS Embedding of CSP to Verify Authentication Protocols.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Thomas Santen	A Theory of Structured Model-Based Specifications in Isabelle/HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Sten Agerholm, Jacob Frost	An Isabelle-Based Theorem Prover for VDM-SL.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Doron A. Peled	Verification for Robust Specification.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Daniel Hirschkoff	A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	James H. Andrews	Executing Formal Specifications by Translation to Higher Order Logic Programming.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Oscar Slotosch	Higher Order Quotients and their Implementation in Isabelle HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Konrad Slind	Derivation and Use of Induction Schemes in Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Myla Archer, Constance L. Heitmeyer	Human-Style Theorem Proving Using PVS.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Martin Simons 0001	Proof Presentation for Isabelle.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Boutheina Chetali, Barbara Heyd	Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis.	TPHOLs	1997	DBLP DOI BibTeX RDF	theorem prover methodology, Larch Prover, Computer Checked Proof, Formal Verification, Unity, Coq
1	Vincent Zammit	A Comparative Study of Coq and HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Elsa L. Gunter, Amy P. Felty (eds.)	Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings	TPHOLs	1997	DBLP DOI BibTeX RDF
1	John Harrison 0001	Verifying the Accuracy of Polynomial Approximations in HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Deepak Kapur	Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Thomas Långbacka, Joakim von Wright	Refining Reactive Systems in HOL Using Action Systems.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Robert L. Constable	ML Programming in Constructive Type Theory (abstract).	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Markus Wenzel 0001	Type Classes and Overloading in Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Gilles Dowek	Proof Normalization for a First-Order Formulation of Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Marco Devillers, W. O. David Griffioen, Olaf Müller	Possibly Infinite Sequences in Theorem Provers: A Comparative Study.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Wolfgang Naraschewski	Towards an Object-Oriented Progification Language.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Takahisa Mohri	On Formalization of Bicategory Theory.	TPHOLs	1997	DBLP DOI BibTeX RDF
1	Cornelia Pusch	Verification of Compiler Correctness for the WAM.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Paul E. Black, Phillip J. Windley	Inference Rules for Programming Languages with Side Effects in Expressions.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Barbara Heyd, Pierre Crégut	A Modular Coding of UNITY in COQ.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Bruno Dutertre	Elements of Mathematical Analysis in PVS.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Linas Laibinis	Using Lattice Theory in Higher Order Logic.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Michael J. Butler, Thomas Långbacka	Program Derivation Using the Refinement Calculator.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	David A. Basin, Stefan Friedrich 0001	Modeling a Hardware Synthesis Methodology in Isabelle.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Sten Agerholm	Translating Specifications in VDM-SL to PVS.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Vincent Zammit	A Mechanisation of Computability Theory in HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	John Harrison 0001	Stålmarck's Algorithm as a HOL Derived Rule.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar	Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Bernhard Reus	Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Stephen H. Brackin	Deciding Cryptographic Protocol Adequacy with HOL: The Implementation.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Solange Coupet-Grimal, Line Jakubiec	Coq and Hardware Verification: A Case Study.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Holger Busch	Proving Liveness of Fair Transition Systems.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Mark R. 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.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Alan Smaill, Ian Green	Higher-Order Annotated Terms for Proof Search.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	John Harrison 0001	A Mizar Mode for HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Sofiène Tahar, Paul Curzon	A Comparison of MDG and HOL for Hardware Verification.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Dieter Nazareth, Tobias Nipkow	Formal Verification of Algorithm W: The Monomorphic Case.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Joakim von Wright, Jim Grundy, John Harrison 0001 (eds.)	Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Michael J. C. Gordon	Set Theory, Higher Order Logic or Both?	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Konrad Slind	Function Definition in Higher-Order Logic.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Sten Agerholm, Ilya Beylin, Peter Dybjer	A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Graham Collins	A Proof Tool for Reasoning About Functional Programs.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Andrew D. Gordon 0001, Thomas F. Melham	Five Axioms of Alpha-Conversion.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Mats Larsson	Improving the Result of High-Level Synthesis Using Interactive Transformational Design.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Douglas J. Howe	Importing Mathematics from HOL into Nuprl.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Kolyang 0001, Thomas Santen, Burkhart Wolff	A Structure Preserving Encoding of Z in Isabelle/HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
1	Graham Collins, Don Syme	A Theory of Finite Maps.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Elsa L. Gunter, Leonid Libkin	Interfacing HOL90 with a Functional Database Query Language.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Ralf Reetz	Deep Embedding VHDL.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Don Syme	A New Interface for HOL - Ideas, Issues and Implementation.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Thomas Långbacka, Rimvydas Ruksenas, Joakim von Wright	TkWinHOL: A Tool for Window Inference in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	E. Thomas Schubert, Phillip J. Windley, Jim Alves-Foss (eds.)	Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Otmane Aït Mohamed	Mechanizing a pi-Calculus Equivalence in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Jean-Paul Bodeveix, Mamoun Filali	On the Refinement of symmetric memory protocols.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Wai Wong	Recording and Checking HOL Proofs.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Paul E. Black, Phillip J. Windley	Autotically Synthesized Term Denotation Predicates: A Proof Aid.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Sten Agerholm, Michael J. C. Gordon	Experiments with ZF Set Theory in HOL and Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl N. Levitt, Ronald A. Olsson	A Hierarchical Method for Reasoning about Distributed Programming Languages.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Morten Welinder	Very Efficient Conversions.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	John Harrison 0001	Floating Point Verification in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	E. Thomas Schubert, Sarah Mocas	A Mechanized Logic for Secure Key Escrow Protocol Verification.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Mitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, Yozo Toda	Formalization of Planar Graphs.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Paul Loewenstein	Formal Verification of Counterflow Pipeline Architecture.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Stephen H. Brackin	Deciding Cryptographic Protocol Adequacy with HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Sten Agerholm	Non-primitive Recursive Function Definitions.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Richard J. Boulton	Combining Decision Procedures in the HOL System.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Paul Curzon	Virtual Theories.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Franz Regensburger	HOLCF: Higher Order Logic of Computable Functions.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Jang Dae Kim, Shiu-Kai Chin	Formal Verification of Serial Pipeline Multipliers.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	John Harrison 0001	Inductive Definitions: Automation and Application.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Dirk Eisenbiegler, Ramayya Kumar	An Automata Theory Dedicated towards Formal Circuit Synthesis.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Holger Busch	A Practical Method for Reasoning about Distributed Systems in a Theorem Prover.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Sara Kalvala	A Formulation of TLA in Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Ching-Tsun Chou	A Formal Theory of Undirected Graphs in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Reasoning About a Class of Linear Systems of Equations in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson	A Graphical Tool for Proving Unity Progress.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Thomas Forster	Weak Systems of Set Theory Related to HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Jeffrey J. Joyce, Nancy A. Day, Michael R. Donat	S: A Machine Readable Specification Notation based on Higher Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Stephen H. Brackin	Providing Tractable Security Analysis in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	David A. Fura, Arun K. Somani	Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Juin-Yeu Lu, Shiu-Kai Chin	Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Paul Curzon	Tracking Design Changes with Formal Verification.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Joakim von Wright	Representing Higher-Order Logic Proofs in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Keith Hanna	Reasoning about Real Circuits.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Sofiène Tahar, Ramayya Kumar	Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Savi Maharaj, Elsa L. Gunter	Studying the ML Module System in Hol.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	N. G. de Bruijn	Highlighting the Lambda-free Fragment of Automath.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Mats Larsson	An Engineering Approach to Formal Digital System Design.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Jean-Paul Bodeveix, Mamoun Filali, P. Roche	Towards a HOL Theory and Memory.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Nick Chapman, Simon Finn, Michael P. Fourman	Datatypes in L2.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Juanito Camilleri, Vincent Zammit	Symbolic Animation as a Proof Tool.	TPHOLs	1994	DBLP DOI BibTeX RDF

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