Program of LFMTP

Wednesday, July 14th

Wednesday's program is also available with abstracts and side by side with other events.

10:25‑10:30 Opening
Location: AT 2.12
10:25 Marino Miculan
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
18:00‑18:10 Closing
Location: AT 2.12
18:00 Marino Miculan