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. (English) Zbl 1391.68001

Lecture Notes in Computer Science 10895. Cham: Springer (ISBN 978-3-319-94820-1/pbk; 978-3-319-94821-8/ebook). xvii, 642 p. (2018).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1369.68009].
Indexed articles:
Achermann, Reto; Humbel, Lukas; Cock, David; Roscoe, Timothy, Physical addressing on real hardware in Isabelle/HOL, 1-19 [Zbl 06946970]
Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas, Towards certified meta-programming with typed Template-Coq, 20-39 [Zbl 1468.68071]
Avelar da Silva, Andréia B.; de Lima, Thaynara Arielly; Galdino, André Luiz, Formalizing ring theory in PVS, 40-47 [Zbl 1451.68332]
Balco, Samuel; Frittella, Sabine; Greco, Giuseppe; Kurz, Alexander; Palmigiano, Alessandra, Software tool support for modular reasoning in modal logics of actions, 48-67 [Zbl 06946973]
Bannister, Callum; Höfner, Peter; Klein, Gerwin, Backwards and forwards with separation logic, 68-87 [Zbl 06946974]
Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E., A Coq formalisation of SQL’s execution engines, 88-107 [Zbl 06946975]
Boulmé, Sylvain; Maréchal, Alexandre, A Coq tactic for equality learning in linear arithmetic, 108-125 [Zbl 06946976]
Baston, Colm; Capretta, Venanzio, The coinductive formulation of common knowledge, 126-141 [Zbl 06946977]
Cauderlier, Raphaël, Tactics and certificates in Meta Dedukti, 142-159 [Zbl 1482.68266]
Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa, A formalization of the LLL basis reduction algorithm, 160-177 [Zbl 1468.68287]
Doczkal, Christian; Combette, Guillaume; Pous, Damien, A formal proof of the minor-exclusion property for treewidth-two graphs, 178-195 [Zbl 1468.68319]
Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias, Verified analysis of random binary tree structures, 196-214 [Zbl 1468.68288]
Carette, Jacques; Farmer, William M.; Laskowski, Patrick, HOL Light QE, 215-234 [Zbl 06946982]
Firsov, Denis; Blair, Richard; Stump, Aaron, Efficient Mendler-style lambda-encodings in cedille, 235-252 [Zbl 06946983]
Forster, Yannick; Heiter, Edith; Smolka, Gert, Verification of PCP-related computational reductions in Coq, 253-269 [Zbl 06946984]
Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef, ProofWatch: watchlist guidance for large theories in E, 270-288 [Zbl 1435.68369]
Gross, Jason; Erbsen, Andres; Chlipala, Adam, Reification by parametricity – fast setup for proof by reflection, in two lines of Ltac, 289-305 [Zbl 06946986]
Jantsch, Simon; Norrish, Michael, Verifying the LTL to Büchi automata translation via very weak alternating automata, 306-323 [Zbl 06946987]
Kahl, Wolfram, CalcCheck: a proof checker for teaching the “Logical approach to discrete math”, 324-341 [Zbl 1462.68215]
Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina, Understanding parameters of deductive verification: an empirical investigation of key, 342-361 [Zbl 06946989]
Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O., Software verification with ITPs should use binary code extraction to reduce the TCB (short paper), 362-369 [Zbl 06946990]
Larchey-Wendling, Dominique, Proof pearl: constructive extraction of cycle finding algorithms, 370-387 [Zbl 06946991]
Lochbihler, Andreas, Fast machine words in Isabelle/HOL, 388-410 [Zbl 06946992]
Lochbihler, Andreas; Schneider, Joshua, Relational parametricity and quotient preservation for modular (co)datatypes, 411-431 [Zbl 06946993]
Mendes, Alexandra; Ferreira, João F., Towards verified handwritten calculational proofs (short paper), 432-440 [Zbl 06946994]
Meßner, Florian; Parsert, Julian; Schöpf, Jonas; Sternagel, Christian, A formally verified solver for homogeneous linear Diophantine equations, 441-458 [Zbl 06946995]
Miquey, Étienne, Formalizing implicative algebras in Coq, 459-476 [Zbl 06946996]
Moscato, Mariano M.; Lopez Pombo, Carlos G.; Muñoz, César A.; Feliú, Marco A., Boosting the reuse of formal specifications, 477-494 [Zbl 1452.68263]
Parsert, Julian; Kaliszyk, Cezary, Towards formal foundations for game theory, 495-503 [Zbl 06946998]
Pizani Flor, João Paulo; Swierstra, Wouter, Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware, 504-522 [Zbl 06946999]
Rizkallah, Christine; Garbuzov, Dmitri; Zdancewic, Steve, A formal equational theory for call-by-push-value, 523-541 [Zbl 06947000]
Syeda, Hira Taqdees; Klein, Gerwin, Program verification in the presence of cached address translation, 542-559 [Zbl 1468.68069]
Tassarotti, Joseph; Harper, Robert, Verified tail bounds for randomized programs, 560-578 [Zbl 06947002]
Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias, Verified memoization and dynamic programming, 579-596 [Zbl 06947003]
Wimmer, Simon; Hölzl, Johannes, \(\text{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper), 597-603 [Zbl 06947004]
Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom, Formalization of a polymorphic subtyping algorithm, 604-622 [Zbl 06947005]
Zmigrod, Ran; Daggitt, Matthew L.; Griffin, Timothy G., An Agda formalization of Üresin & Dubois’ asynchronous fixed-point theory, 623-639 [Zbl 1468.68311]


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
00B25 Proceedings of conferences of miscellaneous specific interest


Zbl 1369.68009
Full Text: DOI