default search action
9th ITP 2018: Oxford, UK
- Jeremy Avigad, Assia Mahboubi:
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Lecture Notes in Computer Science 10895, Springer 2018, ISBN 978-3-319-94820-1 - Reto Achermann, Lukas Humbel
, David A. Cock
Physical Addressing on Real Hardware in Isabelle/HOL. 1-19 - Abhishek Anand, Simon Boulier, Cyril Cohen
Towards Certified Meta-Programming with Typed Template-Coq. 20-39 - Andréia B. Avelar da Silva, Thaynara Arielly de Lima
Formalizing Ring Theory in PVS. 40-47 - Samuel Balco
Software Tool Support for Modular Reasoning in Modal Logics of Actions. 48-67 - Callum Bannister, Peter Höfner, Gerwin Klein:
Backwards and Forwards with Separation Logic. 68-87 - Véronique Benzaken
A Coq Formalisation of SQL's Execution Engines. 88-107 - Sylvain Boulmé, Alexandre Maréchal:
A Coq Tactic for Equality Learning in Linear Arithmetic. 108-125 - Colm Baston, Venanzio Capretta
The Coinductive Formulation of Common Knowledge. 126-141 - Raphaël Cauderlier:
Tactics and Certificates in Meta Dedukti. 142-159 - Jose Divasón
A Formalization of the LLL Basis Reduction Algorithm. 160-177 - Christian Doczkal, Guillaume Combette, Damien Pous:
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. 178-195 - Manuel Eberl
Verified Analysis of Random Binary Tree Structures. 196-214 - Jacques Carette, William M. Farmer, Patrick Laskowski:
HOL Light QE. 215-234 - Denis Firsov
Efficient Mendler-Style Lambda-Encodings in Cedille. 235-252 - Yannick Forster
Verification of PCP-Related Computational Reductions in Coq. 253-269 - Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban:
ProofWatch: Watchlist Guidance for Large Theories in E. 270-288 - Jason Gross, Andres Erbsen, Adam Chlipala:
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. 289-305 - Simon Jantsch, Michael Norrish
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. 306-323 - Wolfram Kahl:
CalcCheck: A Proof Checker for Teaching the "Logical Approach to Discrete Math". 324-341 - Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer:
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. 342-361 - Ramana Kumar, Eric Mullen, Zachary Tatlock
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). 362-369 - Dominique Larchey-Wendling
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. 370-387 - Andreas Lochbihler:
Fast Machine Words in Isabelle/HOL. 388-410 - Andreas Lochbihler, Joshua Schneider:
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes. 411-431 - Alexandra Mendes, João F. Ferreira:
Towards Verified Handwritten Calculational Proofs - (Short Paper). 432-440 - Florian Meßner, Julian Parsert
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. 441-458 - Étienne Miquey
Formalizing Implicative Algebras in Coq. 459-476 - Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú:
Boosting the Reuse of Formal Specifications. 477-494 - Julian Parsert
Towards Formal Foundations for Game Theory. 495-503 - João Paulo Pizani Flor
Verified Timing Transformations in Synchronous Circuits with \lambda \pi -Ware. 504-522 - Christine Rizkallah
A Formal Equational Theory for Call-By-Push-Value. 523-541 - Hira Taqdees Syeda
Program Verification in the Presence of Cached Address Translation. 542-559 - Joseph Tassarotti, Robert Harper:
Verified Tail Bounds for Randomized Programs. 560-578 - Simon Wimmer
Verified Memoization and Dynamic Programming. 579-596 - Simon Wimmer
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). 597-603 - Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers
Formalization of a Polymorphic Subtyping Algorithm. 604-622 - Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin:
An Agda Formalization of Üresin and Dubois' Asynchronous Fixed-Point Theory. 623-639 - Jeremy Avigad, Assia Mahboubi:
Erratum to: Interactive Theorem Proving.
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-03 20:35 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: