- Talks:
- (in order of presentation)
- "Reasoning About Languages with Binding:
Examples, Problems, Solutions?" (workshop mandate) [.pdf]
Randy Pollack (LFCS, University of Edinburgh)
- "Generic capture-avoiding substitution" [.pdf]
James Cheney (LFCS, University of Edinburgh)
- "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?" [.pdf]
Jamie Gabbay (Dept of CS, King's College London)
- "Defining types with binders in HOL" [.pdf]
Michael Norrish (NICTA)
- "Deciding alpha-equivalence inductively" []
Masahiko Sato (Graduate School of Informatics, Kyoto University)
- "On type theory with names and binding" []
Ian Stark (LFCS, University of Edinburgh)
- "Nominal Techniques as an Isabelle/HOL-Theory" [.pdf]
Christian Urban (Mathematical Institute, Ludwig-Maximilian's University)
- (not presented)
- "Two-level meta-reasoning in Coq" []
Amy Felty (SITE, University of Ottawa)
- "Free Sigma-monoids: a higher-order syntax with meta-variables" [.pdf]
Makoto Hamana (Dept of CS, Gunma University)
- "Primitive and some/any proof principles for beta-standardisation" [.pdf]
René Vestergaard (JAIST).
- Challenges:
- Some/any proof theory, René Vestergaard.
- Implementation of a nominal datatype package, Christian Urban
- Can induction principles that have the variable
convention already build in be completely automated?, Christian Urban
- Extend the nominal approach to non-HOL-based theorem provers, such as Coq, Christian Urban
- Program extraction from nominal proofs, Christian Urban
- Nominal logical frameworks, James Cheney
- Exotic binding forms, James Cheney
René Vestergaard
|
