[PL-sem-jr] Talk monday 7/26, 14:00

[Vincent St-Amour]

Mon 7/26 Room WVH166 14:00-16:00

Ian - Going Meta on the Macro

Description: In today's research communities that involve mechanical
proof checkers and programming language theory, there is a large focus
on meta-reasoning, since creating new (possibly sloppy/unsound) logics
for each PL idea is unpalatable, and the notion of variable binding
must still be tackled. In meta-logics/logical frameworks such as
Isabelle, Twelf or Coq, syntax is represented many different ways - a
hint that there is currently no best approach. In this talk I will
describe different binding constructs in meta-logics and how we might
unify them in a meta-meta-logic that introduces the possibility of
reasoning about macros. If there is time, I will talk about how this
opens the possibility for fully describing hygiene formally.