Dear all, We're happy to announce a little workshop / summer school on Coinduction in Type Theory in Le Bourget-du-Lac, near Chambéry, France, from July 3 to July 6, 2017. Everything you need to know should be at http://lama.univ-savoie.fr/~hirschowitz/CoTT2017 , in particular, registration is here http://lama.univ-savoie.fr/~hirschowitz/CoTT2017/registration.php . Briefly, the workshop will revolve around three mini-courses: - Henning Basold: Type Theory Based on Dependent Inductive and Coinductive Types, - Neil Ghani: Coinduction and infinite games, - Rasmus Møgelberg: Guarded dependent type theory with coinductive types. Contributed talks are solicited on theoretical and more applied topics having to do with coinduction and type theory — preferably both! —, particularly those not represented by the invited talks. In the tradition of the Réalisabilité à Chambéry workshop series, the organisers won't organise much, apart from the talks and coffee breaks. In particular, lunch is not organised and registration is free. Some things generally happen spontaneously, like a social dinner and a barbecue near Lake Bourget. The workshop website includes a few hints for accomodation and the like, but please don't hesitate to contact us in case of further questions. Hoping to see you there, Tom Hirschowitz Clovis Eberhart Pierre Hyvernat Rodolphe Lepigre Christophe Raffalli [For admin and other information see: http://www.mta.ca/~cat-dist/ ]