UF IAS 2012 Archive Working Groups

Working groups in several different areas are being organized by participants.

We currently have two active working groups:

1. Coq: all aspects of UF in Coq. Meets Wednesdays 1:30 - 3 in S101. Organized by Andrej Bauer wiki page
2. Informal HoTT. Meets Tuesdays 1:30 - 3 in S101. Organized by Peter Aczel wiki page
3. Homotopy in Type Theory. Meets Thursdays 1:30 - 3 in Simonyi common room or seminar room.

We have also reserved S101 for Fridays 1 - 12:30, which can be used for additional meetings – talk to Steve to organize a meeting. Watch the google calendar for specific meeting times and places.

Some further proposed areas for working groups are:

• Designing a new proof assistant
• Correctness of the new proof assistant
• Syntax, properties, and computational behavior of homotopy type theories
• Semantics of homotopy type theory (with the Univalence Axiom, Higher Inductive Types, etc.)
• Developing homotopy theory in type theory
• Homotopy theory in type theory with nonclassical axioms (e.g. motivated by higher-categorical semantics)
• Doing and speaking about mathematics informally in homotopy type theory

Feel free to organize a group, and to add more suggestions!