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 1511.68021]
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 1511.68301]
Bannister, Callum; Höfner, Peter; Klein, Gerwin, Backwards and forwards with separation logic, 68-87 [Zbl 1511.68067]
Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E., A Coq formalisation of SQL’s execution engines, 88-107 [Zbl 1511.68107]
Boulmé, Sylvain; Maréchal, Alexandre, A Coq tactic for equality learning in linear arithmetic, 108-125 [Zbl 1511.68306]
Baston, Colm; Capretta, Venanzio, The coinductive formulation of common knowledge, 126-141 [Zbl 1508.03038]
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 1511.68307]
Firsov, Denis; Blair, Richard; Stump, Aaron, Efficient Mendler-style lambda-encodings in Cedille, 235-252 [Zbl 1511.68053]
Forster, Yannick; Heiter, Edith; Smolka, Gert, Verification of PCP-related computational reductions in Coq, 253-269 [Zbl 1511.68310]
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 1511.68311]
Jantsch, Simon; Norrish, Michael, Verifying the LTL to Büchi automata translation via very weak alternating automata, 306-323 [Zbl 1511.68335]
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 1511.68317]
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 1511.68320]
Larchey-Wendling, Dominique, Proof pearl: constructive extraction of cycle finding algorithms, 370-387 [Zbl 1511.68322]
Lochbihler, Andreas, Fast machine words in Isabelle/HOL, 388-410 [Zbl 1511.68324]
Lochbihler, Andreas; Schneider, Joshua, Relational parametricity and quotient preservation for modular (co)datatypes, 411-431 [Zbl 1511.68174]
Mendes, Alexandra; Ferreira, João F., Towards verified handwritten calculational proofs (short paper), 432-440 [Zbl 1511.68328]
Meßner, Florian; Parsert, Julian; Schöpf, Jonas; Sternagel, Christian, A formally verified solver for homogeneous linear Diophantine equations, 441-458 [Zbl 1511.68329]
Miquey, Étienne, Formalizing implicative algebras in Coq, 459-476 [Zbl 1511.68336]
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 1511.68337]
Pizani Flor, João Paulo; Swierstra, Wouter, Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware, 504-522 [Zbl 1511.68023]
Rizkallah, Christine; Garbuzov, Dmitri; Zdancewic, Steve, A formal equational theory for call-by-push-value, 523-541 [Zbl 1511.68086]
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 1511.68342]
Wimmer, Simon; Hu, Shuwei; Nipkow, Tobias, Verified memoization and dynamic programming, 579-596 [Zbl 1511.68094]
Wimmer, Simon; Hölzl, Johannes, \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper), 597-603 [Zbl 1511.68142]
Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom, Formalization of a polymorphic subtyping algorithm, 604-622 [Zbl 1511.68059]
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