default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID7. ITP 2016: Nancy, France
- Jasmin Christian Blanchette, Stephan Merz:
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science 9807, Springer 2016, ISBN 978-3-319-43143-7
Regular Contributions
- Mohammad Abdulaziz, Lawrence C. Paulson
:
An Isabelle/HOL Formalisation of Green's Theorem. 3-19 - Mark Adams:
HOL Zero's Solutions for Pollack-Inconsistency. 20-35 - Romain Aïssat, Frédéric Voisin, Burkhart Wolff:
Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths. 36-51 - June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah:
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. 52-68 - Fahad Ausaf, Roy Dyckhoff, Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). 69-86 - Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi:
CoSMed: A Confidentiality-Verified Social Media Platform. 87-106 - Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann:
Mechanical Verification of a Constructive Proof for FLP. 107-122 - Joachim Breitner:
Visual Theorem Proving with the Incredible Proof Machine. 123-139 - Hing-Lun Chan, Michael Norrish:
Proof Pearl: Bounding Least Common Multiples with Triangles. 140-150 - Christian Doczkal, Gert Smolka:
Two-Way Automata in Coq. 151-166 - Thomas Grégoire, Adam Chlipala:
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. 167-183 - Fabian Immler, Christoph Traut:
The Flow of ODEs. 184-199 - Ondrej Kuncar, Andrei Popescu:
From Types to Sets by Local Type Definitions in Higher-Order Logic. 200-218 - Peter Lammich, S. Reza Sefidgar:
Formalizing the Edmonds-Karp Algorithm. 219-234 - Wenda Li, Lawrence C. Paulson:
A Formal Proof of Cauchy's Residue Theorem. 235-251 - Andreas Lochbihler, Joshua Schneider:
Equational Reasoning with Applicative Functors. 252-273 - Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote:
Formally Verified Approximations of Definite Integrals. 274-289 - Julian Nagele, Aart Middeldorp:
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. 290-306 - Tobias Nipkow:
Automatic Functional Correctness Proofs for Functional Search Trees. 307-322 - Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein:
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. 323-340 - Anders Schlichtkrull:
Formalization of the Resolution Calculus for First-Order Logic. 341-357 - Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov:
Verified Operational Transformation for Trees. 358-373 - Gert Smolka, Kathrin Stark:
Hereditarily Finite Sets in Constructive Type Theory. 374-390 - René Thiemann, Akihisa Yamada:
Algebraic Numbers in Isabelle/HOL. 391-408 - Paolo Torrini:
Modular Dependent Induction in Coq, Mendler-Style. 409-424 - Simon Wimmer:
Formalized Timed Automata. 425-440 - Bohua Zhan:
AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic. 441-456
Rough Diamonds
- David Aspinall, Cezary Kaliszyk:
What's in a Theorem Name? 459-465 - Paul Brunet, Damien Pous, Insa Stucke:
Cardinalities of Finite Relations in Coq. 466-474 - Johannes Hölzl:
Formalising Semantics for Expected Running Time of Probabilistic Programs. 475-482 - Adnan Rashid, Osman Hasan:
On the Formalization of Fourier Transform in Higher-order Logic. 483-490 - Kenneth Roe, Scott F. Smith:
CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond). 491-499
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 2025-12-12 22:52 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:
