CPP 2018

24 papers

1. A Coq formalization of normalization by evaluation for Martin-Löf type theory · Pawel Wieczorek, Dariusz Biernacki
2. A constructive formalisation of Semi-algebraic sets and functions · Boris Djalal
3. A formal proof in Coq of a control function for the inverted pendulum · Damien Rouhling
4. A monadic framework for relational verification: applied to information security, program equivalence, and optimizations · Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko + 4 more
5. A two-level logic perspective on (simultaneous) substitutions · Kaustuv Chaudhuri
6. A verified SAT solver with watched literals using imperative HOL · Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich
7. Adapting proof automation to adapt proofs · Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman
8. Binder aware recursion over well-scoped de Bruijn syntax · Jonas Kaiser, Steven Schäfer, Kathrin Stark
9. Completeness and decidability of converse PDL in the constructive type theory of Coq · Christian Doczkal, Joachim Bard
10. Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper) · Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada
11. Finite sets in homotopy type theory · Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide
12. Formal microeconomic foundations and the first welfare theorem · Cezary Kaliszyk, Julian Parsert
13. Formal proof of polynomial-time complexity with quasi-interpretations · Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak
14. Generic derivation of induction for impredicative encodings in Cedille · Denis Firsov, Aaron Stump
15. HOπ in Coq · Sergueï Lenglet, Alan Schmitt
16. Large model constructions for second-order ZF in dependent type theory · Dominik Kirst, Gert Smolka
17. Mechanising and verifying the WebAssembly specification · Conrad Watt
18. Mechanising blockchain consensus · George Pîrlea, Ilya Sergey
19. POPLMark reloaded: mechanizing logical relations proofs (invited talk) · Brigitte Pientka
20. Proofs in conflict-driven theory combination · Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
21. Total Haskell is reasonable Coq · Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
22. Towards verifying ethereum smart contract bytecode in Isabelle/HOL · Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples
23. Triangulating context lemmas · Craig McLaughlin, James McKinna, Ian Stark
24. Œuf: minimizing the Coq extraction TCB · Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman