POPL 2017 (series) / CPP 2017 (series) /
CPP 2017 Program
This is the CPP 2017 program - see the full program for POPL 2017 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Porting the HOL Light Analysis Library: Some Lessons CPP Lawrence Paulson University of Cambridge File Attached |
10:30 - 12:00 | |||
10:30 30mTalk | Verifying a hash table and its iterators in higher-order separation logic CPP | ||
11:00 30mTalk | A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP | ||
11:30 30mTalk | Formal foundations of 3D geometry for modeling robot manipulators CPP |
14:00 - 15:30 | |||
14:00 30mTalk | BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP | ||
14:30 30mTalk | Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP | ||
15:00 30mTalk | Formalization of Karp-Miller Tree Construction on Petri Nets CPP |
16:00 - 18:00 | |||
16:00 30mTalk | A Coq Formal Proof of the Lax–Milgram theorem CPP | ||
16:30 30mTalk | A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP | ||
17:00 30mTalk | Markov Processes in Isabelle/HOL CPP Johannes Hölzl Technische Universität München DOI Pre-print File Attached | ||
17:30 30mTalk | Formalising Real Numbers in Homotopy Type Theory CPP |
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Mechanized verification of preemptive OS kernels CPP Xinyu Feng University of Science and Technology of China File Attached |
10:30 - 12:00 | |||
10:30 30mTalk | Verified compilation of CakeML to multiple machine-code targets CPP Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar | ||
11:00 30mTalk | COMPLX: a verification framework for concurrent imperative programs CPP Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin , Corey Lewis , Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong | ||
11:30 30mTalk | Verifying dynamic race detection CPP William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania |
14:00 - 15:30 | |||
14:00 30mTalk | The HoTT library: a formalization of homotopy type theory in Coq CPP Andrej Bauer University of Ljubljana, Jason Gross MIT CSAIL, Peter Lefanu Lumsdaine , Michael Shulman , Matthieu Sozeau Inria, Bas Spitters Pre-print | ||
14:30 30mTalk | Lifting proof-relevant unification to higher dimensions CPP | ||
15:00 30mTalk | The Next 700 Syntactical models of type theory CPP |
16:00 - 17:30 | |||
16:00 30mTalk | Type-and-scope safe programs and their proofs CPP Guillaume Allais Radboud University Nijmegen, James Chapman , Conor McBride , James McKinna University of Edinburgh | ||
16:30 30mTalk | Formally verified differential dynamic logic CPP | ||
17:00 30mTalk | Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP |