Wednesday, July 14th
Wednesday's program is also available with abstracts and side by side with other events.
10:30‑12:30 Formalizations
Chair: Amy Felty
Location: AT 2.12
| 10:30 | Dan Licata and Robert Harper A Monadic Formalization of ML5 |
| 11:00 | Herman Geuvers, Robbert Krebbers, James McKinna and Freek Wiedijk Pure Type Systems without Explicit Contexts |
| 11:30 | Florian Rabe Representing Isabelle in LF |
| 12:00 | Andreas Abel and Brigitte Pientka Explicit substitutions for contextual type theory |
14:00‑15:00 Implementations
Chair: Andy Pitts
Location: AT 2.12
| 14:00 | Anders Schack-Nielsen and Carsten Schuermann Pattern Unification for the Lambda Calculus with Linear and Affine Types |
| 14:30 | Maribel Fernandez and Murdoch Gabbay Closed nominal rewriting and efficiently computable nominal algebra equality |
15:30‑17:00 HOAS and Invited Speaker 1
Chair: Carsten Schuermann
Location: AT 2.12
| 15:30 | John Boyland Generating Bijections between HOAS and the Natural Numbers |
| 16:00 | Chung-chieh Shan (Rutgers, The State University of New Jersey) Typed metaprogramming with effects |
17:00‑18:00 Invited speaker 2
Chair: Marino Miculan
Location: AT 2.12
| 17:00 | Frank Pfenning (Carnegie Mellon University) The Practice and Promise of Substructural Frameworks |