CPP 2017
21 papers
- A Coq formal proof of the LaxMilgram theorem
- A formalization of the Berlekamp-Zassenhaus factorization algorithm
- A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations
- Automatic cyclic termination proofs for recursive procedures in separation logic
- BliStrTune: hierarchical invention of theorem proving strategies
- Complx: a verification framework for concurrent imperative programs
- Equivalence of system f and ź2 in Coq based on context morphism lemmas
- Formal foundations of 3D geometry to model robot manipulators
- Formalising real numbers in homotopy type theory
- Formalization of Karp-Miller tree construction on petri nets
- Formally verified differential dynamic logic
- Lifting proof-relevant unification to higher dimensions
- Markov processes in Isabelle/HOL
- Mechanized verification of preemptive OS kernels (invited talk)
- Porting the HOL light analysis library: some lessons (invited talk)
- The HoTT library: a formalization of homotopy type theory in Coq
- The next 700 syntactical models of type theory
- Type-and-scope safe programs and their proofs
- Verified compilation of CakeML to multiple machine-code targets
- Verifying a hash table and its iterators in higher-order separation logic
- Verifying dynamic race detection