1:00pm

Welcome!

2:00pm

Francisco Ferreira. Dependent Type Theory with Contextual Types

2:30pm

Stefan Monnier. Typer: An infix statically typed Lisp

3:00pm

François Thiré. Sharing Arithmetic Proofs from Dedukti to HOL

3:30pm

Break

4:30pm

Samuel Gélineau. Incidental dependencies in a client/server architecture

5:00pm

James Shubin. Next Generation Config Mgmt: The Language

5:30pm

Masahiko Sato. A common notation system for both lambda calculus and combinatory logic

6:00pm

Dinner and Drinks!

1:00pm

Welcome!

1:30pm

David Thibodeau. A Mechanization of Howe's Method in Beluga

2:00pm

Vincent Archambault. Metaprogramming and Dependent Types

2:30pm

Break

3:30pm

Stefan Knudsen. An Introduction to Mendler-style (Co)Recursion

4:00pm

Zhentao Li. Making graphical interfaces from geometric primitives