default search action

combined dblp search
author search
venue search
publication search

ask others

5. ITP 2014: Vienna, Austria

> Home > Conferences and Workshops > ITP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/itp/2014
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/2014
Gerwin Klein, Ruben Gamboa:
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in Computer Science 8558, Springer 2014, ISBN 978-3-319-08969-0

Invited Papers

- view
  authority control:
- export record
  dblp key:
  - conf/itp/DavisSS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DavisSS14
Jared Davis, Anna Slobodová, Sol Swords:
Microcode Verification - Another Piece of the Microprocessor Verification Puzzle. 1-16
- view
  authority control:
- export record
  dblp key:
  - conf/itp/ChapmanS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ChapmanS14
Roderick Chapman, Florian Schanda:
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. 17-26

Regular Papers

- view
  authority control:
- export record
  dblp key:
  - conf/itp/AnandR14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AnandR14
Abhishek Anand, Vincent Rahli:
Towards a Formally Verified Proof Assistant. 27-44
- view
  authority control:
- export record
  dblp key:
  - conf/itp/AravantinosT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AravantinosT14
Vincent Aravantinos, Sofiène Tahar:
Implicational Rewriting Tactics in HOL. 45-60
- view
  authority control:
- export record
  dblp key:
  - conf/itp/AvigadLR14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AvigadLR14
Jeremy Avigad, Robert Y. Lewis, Cody Roux:
A Heuristic Prover for Real Inequalities. 61-76
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BartziaS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BartziaS14
Evmorfia-Iro Bartzia, Pierre-Yves Strub:
A Formal Library for Elliptic Curves in the Coq Proof Assistant. 77-92
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlanchetteHLP0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchetteHLP0T14
Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel:
Truly Modular (Co)datatypes for Isabelle/HOL. 93-110
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Blanchette0T14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Blanchette0T14
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Cardinals in Isabelle/HOL. 111-127
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BlazyLP14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlazyLP14
Sandrine Blazy, Vincent Laporte, David Pichardie:
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. 128-143
- view
  authority control:
- export record
  dblp key:
  - conf/itp/BourkeGH14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BourkeGH14
Timothy Bourke, Rob J. van Glabbeek, Peter Höfner:
Showing Invariance Compositionally for a Process Algebra for Network Protocols. 144-159
- view
  authority control:
- export record
  dblp key:
  - conf/itp/ChyzakMST14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ChyzakMST14
Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi:
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). 160-176
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Cock14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Cock14
David A. Cock:
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle. 177-192
- view
  authority control:
- export record
  dblp key:
  - conf/itp/CohenM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/CohenM14
Cyril Cohen, Anders Mörtberg:
A Coq Formalization of Finitely Presented Modules. 193-208
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Dockins14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Dockins14
Robert Dockins:
Formalized, Effective Domain Theory in Coq. 209-225
- view
  authority control:
- export record
  dblp key:
  - conf/itp/DoczkalS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DoczkalS14
Christian Doczkal, Gert Smolka:
Completeness and Decidability Results for CTL in Coq. 226-241
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Dufourd14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Dufourd14
Jean-François Dufourd:
Hypermap Specification and Certified Linked Implementation Using Orbits. 242-257
- view
  authority control:
- export record
  dblp key:
  - conf/itp/EmotoLT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/EmotoLT14
Kento Emoto, Frédéric Loulergue, Julien Tesson:
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. 258-274
- view
  authority control:
- export record
  dblp key:
  - conf/itp/GrossCS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/GrossCS14
Jason Gross, Adam Chlipala, David I. Spivak:
Experience Implementing a Performant Category-Theory Library in Coq. 275-291
- view
  authority control:
- export record
  dblp key:
  - conf/itp/HirokawaMS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/HirokawaMS14
Nao Hirokawa, Aart Middeldorp, Christian Sternagel:
A New and Formalized Proof of Abstract Completion. 292-307
- view
  authority control:
- export record
  dblp key:
  - conf/itp/KumarAMO14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KumarAMO14
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens:
HOL with Definitions: Semantics, Soundness, and a Verified Implementation. 308-324
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Lammich14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Lammich14
Peter Lammich:
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm. 325-340
- view
  authority control:
- export record
  dblp key:
  - conf/itp/LochbihlerH14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LochbihlerH14
Andreas Lochbihler, Johannes Hölzl:
Recursive Functions on Lazy Lists via Domains and Topologies. 341-357
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MahmoudAT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MahmoudAT14
Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar:
Formal Verification of Optical Quantum Flip Gate. 358-373
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MalechaCB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MalechaCB14
Gregory Malecha, Adam Chlipala, Thomas Braibant:
Compositional Computational Reflection. 374-389
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MatichukWM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MatichukWM14
Daniel Matichuk, Makarius Wenzel, Toby C. Murray:
An Isabelle Proof Method Language. 390-405
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Moore14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Moore14
J Strother Moore:
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. 406-420
- view
  authority control:
- export record
  dblp key:
  - conf/itp/MyreenD14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MyreenD14
Magnus O. Myreen, Jared Davis:
The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). 421-436
- view
  authority control:
- export record
  dblp key:
  - conf/itp/NavesS14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/NavesS14
Guyslain Naves, Arnaud Spiwack:
Balancing Lists: A Proof Pearl. 437-449
- view
  authority control:
- export record
  dblp key:
  - conf/itp/NipkowT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/NipkowT14
Tobias Nipkow, Dmitriy Traytel:
Unified Decision Procedures for Regular Expression Equivalence. 450-466
- view
  authority control:
- export record
  dblp key:
  - conf/itp/RingL14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/RingL14
Martin Ring, Christoph Lüth:
Collaborative Interactive Theorem Proving with Clide. 467-482
- view
  authority control:
- export record
  dblp key:
  - conf/itp/SiddiqueMT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/SiddiqueMT14
Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar:
On the Formalization of Z-Transform in HOL. 483-498
- view
  authority control:
- export record
  dblp key:
  - conf/itp/SozeauT14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/SozeauT14
Matthieu Sozeau, Nicolas Tabareau:
Universe Polymorphism in Coq. 499-514
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Wenzel14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Wenzel14
Makarius Wenzel:
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. 515-530

Rough Diamonds

- view
  authority control:
- export record
  dblp key:
  - conf/itp/Arthan14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Arthan14
Rob Arthan:
HOL Constant Definition Done Right. 531-536
- view
  authority control:
- export record
  dblp key:
  - conf/itp/KaufmannM14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KaufmannM14
Matt Kaufmann, J Strother Moore:
Rough Diamond: An Extension of Equivalence-Based Rewriting. 537-542
- view
  authority control:
- export record
  dblp key:
  - conf/itp/KrebbersLW14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KrebbersLW14
Robbert Krebbers, Xavier Leroy, Freek Wiedijk:
Formal C Semantics: CompCert and the C Standard. 543-548
- view
  authority control:
- export record
  dblp key:
  - conf/itp/PuriRHX14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/PuriRHX14
Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie:
Mechanical Certification of Loop Pipelining Transformations: A Preview. 549-554

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.