Journée « égalité et terminaison » du 2 février 2010
Venue: La Ciotat (see JFLA 2010)
Programme 13:30 - 18:00:
Programme 13:30 - 18:00:
- Pierre-Yves Strub (CoqMT)
- Pierre Corbineau (Intégrer l'axiome K de Streicher dans le CIC)
- Bruno Barras (Reminder of current termination checking algorithm)
- Benjamin Gregoire and Jorge-Luis Sacchini (Type based termination dans Coq)
- Andreas Abel (Integration of type based termination with implicit quantification and proof irrelevance)