Information of Workshop

Title: Binding Challenges

Topic: Formal reasoning about languages with binding: examples, problems, solutions

Description:

Doing formal reasoning about languages with binding (such as, e.g., most programming languages) is far from as straightforward as it appears or even ought to be. The problem is how to adapt the induction and recursion principles that exist primitively for all abstract syntax to respect the static scoping of binders. Formally speaking, doing too little or too much immediately result in inconsistent theories.

In spite of several decades of awareness of the problems, it is only in the last 5 or so years that formally underpinned tools and techniques have emerged. The challenge we are faced with now is to make them practically useful. The mandate of the workshop is to produce a reference list of what this might mean in concrete terms.

Sun, Apr. 24
============

10:00: Welcome + mandate of workshop, Randy Pollack, CoE, JAIST (by proxy)

10:15: "Generic capture-avoiding substitution", James Cheney (LFCS, University of Edinburgh, UK)

11:15: "Two-Level Meta-Reasoning in Coq", Amy Felty (SITE, University of Ottawa, CND)

12:15: lunch break

13:30: "Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class "type", without having to rewrite the whole thing from scratch --- yes or no?", Jamie Gabbay (Dept of CS, King's College London, UK)

14:30: "Implementing binding datatypes in HOL", Michael Norrish (NICTA, Canberra, AUS)

15:30: Coffee break

16:00: "Deciding $\alpha$-equivalence inductively", Masahiko Sato (Graduate School of Informatics, Kyoto University, JP)

===

Mon, Apr. 25
============

09:45: "On type theory with names and binding", Ian Stark (LFCS, University of Edinburgh, UK)

10:45: short break

11:00: "A Formal Treatment of the Barendregt's Variable Convention", Christian Urban (Math Institute, LMU, Munich, DE)

12:00: lunch break

13:00: "Free Sigma-monoids: A Higher-Order Syntax with Metavariables", Makoto Hamana (Dept of CS, Gunma University, JP)

14:00: "Primitive and Some/Any Proof Principles for beta-Standardisation", Rene Vestergaard (JAIST, JP)

15:00: Coffee and round-table discussion in I74

17:00: End