Semantics of proofs and certified mathematics, Institut Henri Poincaré, April 22nd - July 11th, 2014, organized by Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès.
If you like applications of category theory to logic and computer science, there should be a lot for you here!
Week 1 — Kick-off: Formalisation in mathematics and in computer science
Week 3 — Workshop 1: Formalization of mathematics in proof assistants, organized by Georges Gonthier and Vladimir Voevodsky.
Week 6 — Workshop 2: Constructive mathematics and models of type theory, organized by Thierry Coquand and Thomas Streicher.
Week 8 — Workshop 3: Semantics of proofs and programs, organized by Thomas Ehrhard and Alex Simpson.
Week 10 — Workshop 4: Abstraction and verification in semantics, organized by Paul-André Melliès and Luke Ong.
Week 12 — Workshop 5, Certification of high-level and low-level programs organized by Christine Paulin and Zhong Shao.
A lot of people I know will attend parts of this, such as Jean Benabou, Marcelo Fiore, Dan Ghica, André Joyal, Samuel Mimram, and Bas Spitters. And that makes me happy, because Paul-André Melliès has invited me to spend up to a month attending this series of workshops, perhaps in two 2-week stretches. With a little luck I’ll be able to actually do this.
(My wife Lisa Raphals has gotten invited to Erlangen for the spring of 2014, meaning roughly April 1 - June 1. If she and I succeed in getting leaves of absence, I’ll go with her, and then take some trips to nearby places. Since I split my time between the Wild West and the Far East, Paris seems nearby to Erlangen to me. I also have vague invitations to IHES, Prague and Berlin which I might try to take advantage of. And if you have a luxurious villa in northern Italy or the French Riviera, let me know.)
DIGITAL JUICE
No comments:
Post a Comment
Thank's!