coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq Andes Summer School (Jan 2020, Chile)

From: Éric Tanter <etanter AT dcc.uchile.cl>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Coq Andes Summer School (Jan 2020, Chile)
Date: Mon, 23 Sep 2019 14:13:43 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=etanter AT dcc.uchile.cl; spf=Pass smtp.mailfrom=etanter AT dcc.uchile.cl; spf=None smtp.helo=postmaster AT sunsite.dcc.uchile.cl
Dkim-filter: OpenDKIM Filter v2.11.0 sunsite.dcc.uchile.cl x8NCDldd023094
Ironport-phdr: 9a23:PELzKB04MCLkG0hksmDT+DRfVm0co7zxezQtwd8ZseIWL/ad9pjvdHbS+e9qxAeQG9mCsLQe26GK4+igATVGvc/b9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMuMQam5VuJ6U+xhbGoXZDZuBayX91KV6JkBvw+9m88IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRBDIygYIQBEukPM+hGoYf6vFYBtweyBQy2CePv1jNFhHn71rA63eQ7FgHG2RQtGs4UsHTVsNr6LLkcXvqzzKnU0zrDde5d1DDj54jUaB8hp+2MUqxqccfK1EYgCx/Kgk+NqYP5PzOV1+ANvHaB4+V8UeKikmgqoBx/rDiow8cjkIjJhoQNx1Dc8SV23oc1KselR0JhfdGkFJ1dvDyZOYtuWs4uXX1ktDogxrACo5K2eCwHxI46yxPbafGLa5WE7gzgWeqLJTp1imhpdbGhixqo70Ss1+7xW8+p21hQtCVFiMPDtnUV2hzT9MeHTvx981+62TaS0QDT8eBEIVwqmqbBNpEu3qI/moAOsUvfHi/2mUH2g7GMeko4/uik8+XnYrP4qZ+AL4J4lB3yPrg0lsG7G+g1NgwDU3KG9em41rDv5Uj5T69Ljv0ynKnZqpfaJcEDq6GnHw9ayIAj6wqhADe8y9kXgGUII05fdBKak4fpO1DOIPTmAvuln1uslC9nx+raMb35HpXNMn/Dna/9crZ68k5Q0RY8zdRC551PEbwBO/LyWkrptNPCFBM5Mgq0w/zmCNpnzI8eV3iPUeelN/bZtkbN7eYyKaHYb4gM/T35NvIN5vj0jHZ/l0VLLoez2p5CyWq5FcNaKkOFbGCk1todGGEWsxAWQOfhzkCJUT9XajC5W/RvtXkAFIu6ANKbFciWi7ub0XLjR8EEViV9ElmJVEzQWcCcQf5VNXCeKcQnjzcEVLysDYQlh0n36V3KjoF/J++RwRU28JLu0N8vvL/IiBcp9CB5SciW2CeQRGF1mm5OTDtkhPku83w48U+K1O1Du9IdENVS4/1TVQJjaMzQxOc8FtvyWwbMONyNGg+r

Coq Andes Summer School

January 6-10, 2020

Cajón del Maipo, Chile

https://cass.pleiad.cl

The Coq Andes Summer School (CASS) 2020 is a one-week immersive summer school on type theory in general, and on the Coq proof assistant in particular.

CASS is open to advanced and motivated undergraduate and postgraduate students, as well as young academics and professionals. We welcome applications from all over the world. Lectures will be in English.

Registration, shared housing and food are all covered by our projects and sponsors. We also have limited funding to help selected participants traveling from abroad and from outside of the central region of Chile.

Application deadline: October 20, 2019 (AoE)

Check out details and apply: https://cass.pleiad.cl

Speakers

- Assia Mahboubi (Inria, FR): Introduction to Coq & SSReflect

- Matthieu Sozeau (Inria, FR): Programming with dependent types

- Beta Ziliani (U. Córdoba, AR): Tactic languages

- Nicolas Tabareau (Inria, FR): Homotopy type theory

- Alexandre Miquel (U. La República, UR): Realizability

- Pierre-Marie Pédrot (Inria, FR): Exceptional type theory

- Guillaume Munch-Maccagnoni (Inria, FR): Call-by-push-value

Organizers

- Nicolas Tabareau (Inria, FR)

- Éric Tanter (U. Chile, CL)

Funded by

- Projects: ERC CoqHoTT, CONICYT Redes CSEC, Inria Équipe Associée GECO

- Sponsors: NIC Chile, Inria Chile

[Coq-Club] Coq Andes Summer School (Jan 2020, Chile), Éric Tanter, 09/23/2019