Search results for "TPHOLs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	J Strother Moore, Qiang Zhang	Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo	Proof Pearl: A Formal Proof of Higman's Lemma in ACL2.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	John Harrison 0001	A HOL Theory of Euclidean Space.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Tom Ridge, James Margetson	A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Néstor Cataño	Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Nicolas Oury	Extensionality in the Calculus of Constructions.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Russell O'Connor	Essential Incompleteness of Arithmetic Verified by Coq.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Veronika Ortner, Norbert Schirmer	Verification of BDD Normalization.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Diana Toma, Dominique Borrione	Formal Verification of a SHA-1 Circuit Core Using ACL2.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Peter V. Homeier	A Design Structure for Higher Order Quotients.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	César A. Muñoz, David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Michael Norrish, Konrad Slind	Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Julien Schmaltz, Dominique Borrione	A Generic Network on Chip Model.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Mauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, Wolfgang J. Paul	On the Correctness of Operating System Kernels.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Christoph Benzmüller, Chad E. Brown	A Structured Set of Higher-Order Problems.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Hasan Amjad	Shallow Lazy Proofs.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Martin Wildmoser, Tobias Nipkow	Certifying Machine Code Safety: Shallow Versus Deep Embedding.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Einar Broch Johnsen, Christoph Lüth	Theorem Reuse by Proof Term Transformation.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.)	Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings	TPHOLs	2004	DBLP DOI BibTeX RDF
1	David Aspinall 0001, Lennart Beringer, Martin Hofmann 0001, Hans-Wolfgang Loidl, Alberto Momigliano	A Program Logic for Resource Verification.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Stefan Richter 0001	Formalizing Integration Theory with an Application to Probabilistic Algorithms.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Behzad Akbarpour, Sofiène Tahar	Error Analysis of Digital Filters Using Theorem Proving.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Michael Norrish	Recursive Function Definition for Types with Binders.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Thomas C. Hales	Formalizing the Proof of the Kepler Conjecture.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Jean-François Monin	Proof Pearl: From Concrete to Functional Unparsing.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Lee Pike, Jeffrey Maddalon, Paul S. Miner, Alfons Geser	Abstractions for Fault-Tolerant Distributed System Verification.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Jason Hickey, Aleksey Nogin	Extensible Hierarchical Tactic Construction in a Logical Framework.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Michael Jones, Aaron Benson, Dan Delorey	Proving Compatibility Using Refinement.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Tian-jun Zuo, Jun-gang Han, Ping Chen	Formalizing Java Dynamic Loading in HOL.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Luís Cruz-Filipe, Freek Wiedijk	Hierarchical Reflection.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Nadeem Abdul Hamid, Zhong Shao	Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Olivier Boite	Proof Reuse with Extended Inductive Types.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Hanbing Liu, J Strother Moore	Java Program Verification via a JVM Deep Embedding in ACL2.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	John Longley, Randy Pollack	Reasoning About CBV Functional Programs in Isabelle/HOL.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Julien Narboux	A Decision Procedure for Geometry in Coq.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Ting Zhang 0001, Henny B. Sipma, Zohar Manna	Term Algebras with Length Function and Bounded Quantifier Alternation.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Lucas Dixon, Jacques D. Fleuriot	Higher Order Rippling in IsaPlanner.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Ruben Gamboa, John R. Cowles	A Mechanical Proof of the Cook-Levin Theorem.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Al Davis	Correct Embedded Computing Futures.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Penny Anderson, Frank Pfenning	Verifying Uniqueness in a Logical Framework.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Laura I. Meikle, Jacques D. Fleuriot	Formalizing Hilbert's Grundlagen in Isabelle/Isar.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu	MetaPRL - A Modular Logical Environment.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Nicolas Magaud	Changing Data Representation within the Coq System.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Jason Reed 0001	Extending Higher-Order Unification to Support Proof Irrelevance.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Michael Norrish	Complete Integer Decision Procedures as Derived Rules in HOL.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Hasan Amjad	Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Freek Wiedijk, Jan Zwanenburg	First Order Logic with Domain Conditions.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	June Andronick, Boutheina Chetali, Olivier Ly	Using Coq to Verify Java Card Applet Isolation Properties.	TPHOLs	2003	DBLP DOI BibTeX RDF	Security, Theorem Proving, Smart Card
1	Dale Miller 0001	Reasoning about Proof Search Specifications: An Abstract.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Jacek Chrzaszcz	Implementing Modules in the Coq System.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	David Cachera, David Pichardie	Embedding of Systems of Affine Recurrence Equations in Coq.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Deepak Kapur, Nikita A. Sakhanenko	Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson	Verifying Second-Level Security Protocols.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Sava Krstic, John Matthews	Inductive Invariants for Nested Recursion.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Anthony C. J. Fox	Formal Specification and Verification of ARM6.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Claire Louise Quigley	A Programming Logic for Java Bytecode Programs.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	David A. Basin, Burkhart Wolff (eds.)	Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Carsten Schürmann, Frank Pfenning	A Coverage Checking Algorithm for LF.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Gerwin Klein, Martin Wildmoser	Verified Bytecode Subroutines.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Jean-Raymond Abrial, Dominique Cansell	Click'n Prove: Interactive Proofs within Set Theory.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Luís Cruz-Filipe, Bas Spitters	Program Extraction from Large Proof Developments.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Combining Testing and Proving in Dependent Type Theory.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Konrad Slind, Joe Hurd	Applications of Polytypism in Theorem Proving.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Laurent Théry	Proving Pearl: Knuth's Algorithm for Prime Numbers.	TPHOLs	2003	DBLP DOI BibTeX RDF
1	Joe Hurd	A Formal Approach to Probabilistic Termination.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu 0005	Weakest Precondition for General Recursive Programs Formalized in Coq.	TPHOLs	2002	DBLP DOI BibTeX RDF	Formal Verification, Operational Semantics, Weakest Precondition, Coq
1	Gérard P. Huet	Higher Order Unification 30 Years Later.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Gilles Barthe, Pierre Courtieu	Efficient Reasoning about Executable Specifications in Coq.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Klaus Schneider 0001	Proving the Equivalence of Microstep and Macrostep Semantics.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Achim D. Brucker, Burkhart Wolff	A Proposal for a Formal OCL Semantics in Isabelle/HOL.	TPHOLs	2002	DBLP DOI BibTeX RDF	shallow embedding, UML, testing, OCL, Isabelle
1	Louise A. Dennis, Alan Bundy	A Comparison of Two Proof Critics: Power vs. Robustness.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	David Delahaye	Free-Style Theorem Proving.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Yves Bertot, Venanzio Capretta, Kuntal Das Barman	Type-Theoretic Functional Semantics.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Judicaël Courant	Explicit Universes for the Calculus of Constructions.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Amy P. Felty	Two-Level Meta-reasoning in Coq.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Ricky W. Butler	Formal Methods at NASA Langley.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Jeremy E. Dawson, Rajeev Goré	Formalised Cut Admissibility for Display Logic.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Michael J. C. Gordon	PuzzleTool : An Example of Programming Computation and Deduction.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Aleksey Nogin, Jason Hickey	Sequent Schema for Derived Rules.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Simon Ambler, Roy L. Crole, Alberto Momigliano	Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	David A. Basin, Stefan Friedrich 0001, Marek Gawkowski	Verified Bytecode Model Checkers.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Micaela Mayero	Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm).	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Victor Carreño, César A. Muñoz, Sofiène Tahar (eds.)	Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Virgile Prevosto, Damien Doligez, Thérèse Hardin	Algebraic Structures and Dependent Records.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Christophe Dehlinger, Jean-François Dufourd	Formalizing the Trading Theorem for the Classification of Surfaces.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Aleksey Nogin	Quotient Types: A Modular Approach.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Gertrud Bauer, Tobias Nipkow	The 5 Colour Theorem in Isabelle/Isar.	TPHOLs	2002	DBLP DOI BibTeX RDF
1	Venanzio Capretta	Certifying the Fast Fourier Transform with Coq.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Freek Wiedijk	Mizar Light for HOL Light.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez	A Certified Polynomial-Based Decision Procedure for Propositional Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Xavier Rival, Jean Goubault-Larrecq	Experiments with Finite Tree Automata in Coq.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	J Strother Moore	Finite Set Theory in ACL2.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Steven D. Johnson	View from the Fringe of the Fringe (Joint with CHARME 2001).	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Joe Hurd	Predicate Subtyping with Predicate Sets.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Marc Daumas, Laurence Rideau, Laurent Théry	A Generic Library for Floating-Point Numbers and Its Application to Exact Computing.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	David Pichardie, Yves Bertot	Formalizing Convex Hull Algorithms.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Steffen Helke, Florian Kammüller	Representing Hierarchical Automata in Interactive Theorem Provers.	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Richard J. Boulton, Paul B. Jackson (eds.)	Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings	TPHOLs	2001	DBLP DOI BibTeX RDF
1	Simon J. Gay	A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF	semantics, Types, pi calculus, automatic theorem proving

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