VSL 2014: VIENNA SUMMER OF LOGIC 2014
COQ PROGRAM
Friday, July 18th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 86A: New and advanced Coq features
Chair:
Viktor Vafeiadis
Location: MB, Hörsaal 14A
08:45
Jason Gross
Presentation of Three Neat Tricks in Coq 8.5 (abstract)
09:15
Beta Ziliani and Matthieu Sozeau
Towards a better-behaved unification algorithm for Coq (abstract)
09:45
Matthieu Sozeau
Proof-relevant rewriting strategies in Coq (abstract)
10:15-10:45Coffee Break
10:45-12:45 Session 90AC: Invited talk & useful tools
Chair:
Matthieu Sozeau
Location: MB, Hörsaal 14A
10:45
Daniel Licata
What is Homotopy Type Theory? (abstract)
11:45
Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou and Benjamin C. Pierce
QuickChick: Property-Based Testing for Coq (abstract)
12:15
Jónathan Heras and Ekaterina Komendantskaya
Proof-Pattern Search in Coq/SSReflect (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 96AA: Formalizations in Coq
Chair:
Derek Dreyer
Location: MB, Hörsaal 14A
14:30
Reynald Affeldt and Jacques Garrigue
Formalization of Error-correcting Codes using SSReflect (abstract)
15:00
Steven Schäfer, Tobias Tebbi and Gert Smolka
Autosubst: Automation for de Bruijn Substitutions (abstract)
15:30
Gregory Malecha, Jesper Bengtson and Adam Chlipala
Automating Abstract Logics (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 99AA: New IDEs & Coq 8.5 update
Chair:
Antonis Stampoulis
Location: MB, Hörsaal 14A
16:30
Carst Tankink
Asynchronous interaction for Coq (abstract)
17:00
Alexander Faithfull and Jesper Bengtson
Coqoon: towards a modern IDE for Coq (abstract)
17:30
Matthieu Sozeau
Update on Coq 8.5 (abstract)