The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

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

URL (DBLP): http://dblp.uni-trier.de/db/conf/tphol

Publication years (Num. hits)
1991 (40) 1992 (37) 1993-1994 (32) 1995 (27) 1996 (29) 1997 (23) 1998 (29) 1999 (24) 2000 (34) 2001 (27) 2002 (23) 2003 (24) 2004 (24) 2005 (27) 2007 (29) 2008 (26) 2009 (35)
Publication types (Num. hits)
inproceedings(473) proceedings(17)
Venues (Conferences, Journals, ...)
TPHOLs(490)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
The graphs summarize 37 occurrences of 30 keywords

Results
Found 490 publication records. Showing 490 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
1Jesper Bengtson, Joachim Parrow Psi-calculi in Isabelle. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Jeremy E. Dawson, Alwen Tiu Formalising Observer Theory for Environment-Sensitive Bisimulation. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi Hints in Unification. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Wouter Swierstra A Hoare Logic for the State Monad. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Stefan Berghofer, Markus Reiter Formalizing the Logic-Automaton Connection. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Andrew McCreight Practical Tactics for Separation Logic. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Carsten Schürmann The Twelf Proof Assistant. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Ana Bove, Peter Dybjer, Ulf Norell A Brief Overview of Agda - A Functional Language with Dependent Types. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt Let's Get Physical: Models and Methods for Real-World Security Protocols. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish Mind the Gap. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1John Harrison Without Loss of Generality. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Andreas Lochbihler Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Peter V. Homeier The HOL-Omega Logic. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Stefan Berghofer, Lukas Bulwahn, Florian Haftmann Turning Inductive into Equational Specifications. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Keiko Nakata 0001, Tarmo Uustalu Trace-Based Coinductive Operational Semantics for While. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Nick Benton, Andrew Kennedy, Carsten Varming Some Domain Theory and Denotational Semantics in Coq. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Stéphane Le Roux 0001 Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF sequential game theory, effective generalisation, abstraction, induction, Coq
1Jinshuang Wang, Huabing Yang, Xingyuan Zhang Liveness Reasoning with Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model
1Scott Owens, Susmit Sarkar, Peter Sewell A Better x86 Memory Model: x86-TSO. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1René Thiemann, Christian Sternagel Certification of Termination Proofs Using CeTA. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Frédéric Dabrowski, David Pichardie A Certified Data Race Analysis for a Java-like Language. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1John Harrison HOL Light: An Overview. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Javier de Dios, Ricardo Peña-Marí Formal Certification of a Resource-Aware Language Implementation. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF memory management, functional languages, compiler verification
1Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar Formal Analysis of Optical Waveguides in HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Magnus O. Myreen, Michael J. C. Gordon Verified LISP Implementations on ARM, x86 and PowerPC. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Rafal Kolanski, Gerwin Klein Types, Maps and Separation Logic. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Brian Huffman A Purely Definitional Universal Domain. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Nicolas Julien, Ioana Pasca Formal Verification of Exact Computations Using Newton's Method. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Alexander Schimpf, Stephan Merz, Jan-Georg Smaus Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Thomas Tuerk A Formalisation of Smallfoot in HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies VCC: A Practical System for Verifying Concurrent C. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Chad E. Brown, Gert Smolka Extended First-Order Logic. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1Adam Naumowicz, Artur Kornilowicz A Brief Overview of Mizar. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
1François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau Packaging Mathematical Structures. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Formalization of Algebra, Coercive subtyping, SSReflect, Type inference, Coq
1Mike Gordon Twenty Years of Theorem Proving for HOLs Past, Present and Future. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Matt Kaufmann, J Strother Moore An ACL2 Tutorial. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow The Isabelle Framework. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Sam Owre, Natarajan Shankar A Brief Overview of PVS. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca Canonical Big Operators. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Russell O'Connor Certified Exact Transcendental Real Number Computation in Coq. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Steven P. Miller Will This Be Formal? Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF model checking, Formal methods, theorem proving, avionics
1Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Klaus Aehlig, Florian Haftmann, Tobias Nipkow A Compiled Implementation of Normalization by Evaluation. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1David Cock, Gerwin Klein, Thomas Sewell Secure Microkernels, State Monads and Scalable Refinement. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Sayan Mitra, K. Mani Chandy A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Hasan Amjad LCF-Style Propositional Simplification with BDDs and SAT Solvers. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Holger Gast Lightweight Separation. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Jens Brandt 0001, Klaus Schneider 0001 Formal Reasoning About Causality Analysis. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1David R. Lester Real Number Calculations and Theorem Proving. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic
1Daniel Wasserrab, Andreas Lochbihler Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Pierre Courtieu, Julien Forest, Xavier Urbain Certifying a Termination Criterion Based on Graphs, without Graphs. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Laurent Théry Proof Pearl: Revisiting the Mini-rubik in Coq. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews Imperative Functional Programming with Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Ana Bove, Venanzio Capretta A Type of Partial Recursive Functions. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Matthieu Sozeau, Nicolas Oury First-Class Type Classes. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Yves Bertot A Short Presentation of Coq. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks 0001, Iulian Neamtiu Formalizing Soundness of Contextual Effects. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Konrad Slind, Michael Norrish A Brief Overview of HOL4. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Stefan Berghofer, Christian Urban Nominal Inversion Principles. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
1Matt Kaufmann, Konrad Slind Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Christoph Sprenger 0001, David A. Basin A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Michael Norrish, René Vestergaard Proof Pearl: De Bruijn Terms Really Do Work. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Lukas Bulwahn, Alexander Krauss, Tobias Nipkow Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Andrew W. Appel, Sandrine Blazy Separation Logic for Small-Step cminor. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Osman Hasan, Sofiène Tahar Verification of Expectation Properties for Discrete Random Variables in HOL. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Tom Ridge Operational Reasoning for Concurrent Caml Programs and Weak Memory Models. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1James Reynolds Automatically Translating Type and Function Definitions from HOL to ACL2. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1David Aspinall 0001, Jaroslav Sevcík Formalising Java's Data Race Free Guarantee. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Peter Liggesmeyer Formal Techniques in Software Engineering: Correct Software and Safe Systems. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Norbert Völker HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1John Harrison Verifying Nonlinear Real Formulas Via Sums of Squares. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1David Delahaye, Catherine Dubois, Jean-Frédéric Étienne Extracting Purely Functional Contents from Logical Inductive Types. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Eunsuk Kang, Mark Aagaard Improving the Usability of HOL Through Controlled Automation Tactics. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Steven Obua Proof Pearl: Looping Around the Orbit. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1François Garillot, Benjamin Werner Simple Types in Type Theory: Deep and Shallow Encodings. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Zhaozhong Ni, Dachuan Yu, Zhong Shao Using XCAP to Certify Realistic Systems Code: Machine Context Management. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Freek Wiedijk Mizar's Soft Type System. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Lawrence C. Paulson, Kong Woei Susanto Source-Level Proof Reconstruction for Interactive Theorem Proving. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Brigitte Pientka Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina A Formally Verified Prover for the ALC Description Logic. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Yasuhiko Minamide Verified Decision Procedures on Context-Free Grammars. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Klaus Schneider 0001, Jens Brandt 0001 (eds.) Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Makarius Wenzel, Burkhart Wolff Building Formal Method Tools in the Isabelle/Isar Framework. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Jeremy E. Dawson Formalising Generalised Substitutions. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF general correctness, generalised substitution
1Joe Hurd Proof Pearl: The Termination Analysis of Terminator. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry A Modular Formalisation of Finite Group Theory. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Constance L. Heitmeyer On the Utility of Formal Methods in the Development and Certification of Software. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Laurent Théry, Guillaume Hanrot Primality Proving with Elliptic Curves. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
1Veronika Ortner, Norbert Schirmer Verification of BDD Normalization. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Nicolas Oury Extensionality in the Calculus of Constructions. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1David A. Naumann Verifying a Secure Information Flow Analyzer. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1J Strother Moore, Qiang Zhang Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic Mechanized Metatheory for the Masses: The PoplMark Challenge. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Claude Marché, Christine Paulin-Mohring Reasoning About Java Programs with Aliasing and Frame Conditions. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith Meta Reasoning in ACL2. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Peter V. Homeier A Design Structure for Higher Order Quotients. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Russell O'Connor Essential Incompleteness of Arithmetic Verified by Coq. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
1Julien Schmaltz, Dominique Borrione A Generic Network on Chip Model. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #100 of 490 (100 per page; Change: )
Pages: [1][2][3][4][5][>>]
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license