CASS 2020 – Coq Andes Summer School

6 – 10 January, 2020, Chile

6 – 10 January 2020, Chile

Event Date

Jan 6-10, 2020

Event Location

Santuario del Río, San José del Maipo, Chile

Application deadline

October 20, 2019 (AoE)

What is CASS 2020?

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.

Who is it for?

CASS is open to advanced and motivated undergraduate and postgraduate students, as well as young academics and professionals.

Everyone is welcome

We welcome applications from all over the world. Lectures will be in English.

Fully immersive school

Attendance to the complete week is mandatory, from Monday lunch until Friday lunch.

What is covered?

Full-week registration, including shared housing and food, is 450.000 CLP. Thanks to our projects and sponsors, registration is free for students and selected participants.

Travel funding

We have limited funding to help selected participants traveling from abroad and from outside of the central region of Chile.

Assia Mahboubi

Inria Bretagne (FR)
Introduction to Coq/SSReflect

Alexandre Miquel

Universidad de la República (UR)
Realizability

Pierre-Marie Pédrot

Inria Bretagne (FR)
Effects in type theory

Matthieu Sozeau

Inria Paris, IRIF (FR)
Dependent elimination

Nicolas Tabareau

Inria Bretagne, France
Homotopy type theory

Beta Ziliani

Universidad de Córdoba (AR)
Tactic languages

Monday Jan 6

Tuesday Jan 7

Wednesday Jan 8

Thursday Jan 9

Friday Jan 10

Monday

12:00 : Welcome Lunch

14:30 – 16:00 / 16:30 – 18:00 : Introduction to Coq (Assia Mahboubi)
[Lecture: Slides (PDF), JsCoq, Coq file | Exercises: JSCoq, Coq file, Solution (Coq file) | Cheatsheet]

Evening : Coq Install Party

Tuesday

9:30 – 11:00 / 11:30 – 13:00 : Programming with Dependent Types (Matthieu Sozeau)
[Lecture: Slides (PDF) | Exercises: Dependent types (JSCoq), Dependent types (Coq file), Inductives (JSCoq), Inductives (Coq file)]

14:30 – 16:00 : Hands-on Session

16:30 – 18:00 : Tactic languages (Beta Ziliani)
[Exercises: JsCoq, Coq file (+ Supplementary material)]

Wednesday

9:30 – 11:00 : Dependent Elimination (Matthieu Sozeau)
[Lecture: Slides (PDF) | Exercises: Equations (JsCoq), Equations (Coq file), Evaluator (JsCoq), Evaluator (Coq file)]

11:30 – 13:00 : Hands-on Session

14:30 : Meeting in front of reception for walk

16:45 : Meeting in front of reception for zipline (For people participating only to zipline activity)

18:30 : Poster Session (Hotel’s terrace – next to restaurant)

20:00 : Barbecue

Thursday

9:30 – 11:00 / 11:30 – 13:00 : Homotopy Type Theory (Nicolas Tabareau)
[Lecture: Slides (PDF) | Exercises: JsCoq, Coq file]

14:30 – 16:00 : Hands-on Session

16:30 – 18:00 : Set Theory vs. Type Theory (Alexandre Miquel)
[Lecture: Slides (PDF)]

Friday

9:30 – 11:00 : Exceptional Type Theory (Pierre-Marie Pédrot)
[Lecture: Slides (PDF)]

11:30 – 13:00 : Call-by-push-value (Guillaume Munch-Maccagnoni)
[Lecture: Slides (PDF)]

13:00 : Wrap-up & Farewell Lunch

Éric Tanter

Universidad de Chile, Chile
Scientific & local chair

Do I need to know Coq to attend?

No, the school is open to all students interested in learning (more) about Coq. We expect applicants to have general knowledge from final year undergraduate studies in computer science, combined with an interest in programming languages and/or verification and/or logic.

How can I apply?

Application is now closed. We’ve selected 41 out of 95 applicants. You can see the list of participants here.

Can I just show up to attend some lectures?

No, the school is a full-week, immersive event. Interested participants must apply in due time.

What are the housing arrangements?

The school covers housing and food in the Santuario del Río resort for four nights. The checkin is on Monday (including lunch), and the checkout is on Friday (including last meal at noon).
The school can also provide some support as well to cover accommodation in Santiago on Sunday before the School.

How do I get there?

The Santiago international airport (SCL) is well connected to major hubs around the globe.

For your travel plans to get to the school location, there are two main options:

1. you arrive a day or two before the school begins, spend some time in Santiago, and take the bus at Inria Chile on Monday morning (recommended), or
2. you land in SCL on Monday morning and then go directly to the Santuario del Río resort by taking the bus transfer that will be arranged (less recommended)

Please check CASS’s Zulip chat and let us know your arrival/departure information by December 10 (AoE) (sooner is better).

In case you pick Option 1 (recommended), you can find cheap student housing in so-called “hospedajes” in Santiago, as well as reasonably priced hotels. And, of course, Airbnb, with a large range of options, including bedrooms in shared apartments. There are plenty of rooms with prices ranging from 15-20 USD. Finally, you can also stay at the Santuario del Río resort if you wish, however prices might be drastically higher (> 130 USD).
On Monday, we will have transportation from downtown Santiago at 9:30am next to Inria Chile offices, in Las Condes (Av. Apoquindo 2827).

In case you pick Option 2 (less recommended), make sure that your plane arrives early enough that you can get to Santuario del Río by 12 PM for the welcome lunch. From the airport, consider between 1h45-2h by taxi/transfer. This means your plane should land no later than ~9 AM. This might be quite inconvenient (if at all possible), depending on where you’re flying from.
We are arranging a transfer from the airport at 09:30.

Regarding transportation from Santiago to the resort, we will provide buses from either downtown Santiago, or from SCL if some of you pick Option 2. We therefore highly recommend Option 1 to facilitate travel arrangements on Monday. Further details on transportation will be provided as the date closes in.

For the way back, you basically have the same options. We will arrange transportation to go straight to the airport on Friday, leaving the resort by 3 PM (consider up to 2h to arrive to SCL), as well as to go to downtown Santiago (Providencia, Ñuñoa).

Where to stay in Santiago?

We recommend looking for places to stay in Providencia and Ñuñoa. We will provide more detailed recommendations in the following weeks.

Where do I start proving things?

You can start proving things online in Coq using JsCoq!. JsCoq is an interactive, web-based environment for the Coq Theorem prover, developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris).

You can access JsCoq online here, or alternatively, you can download it and run it in your machine from here.

Asia & Europe

North America

South America

Czechia
– Guido Chari, Czech Technical University

Denmark
– Frederik Krogsdal Jacobsen, Technical University of Denmark

France
– Félix Castro, Université de Paris
– Kenji Maillard, Inria

Singapore
– Kiran Gopinathan, National University of Singapore

United Kingdom
– Uma Zalakain, University of Glasgow

Mexico
– Diego Carrillo Verduzco, Universidad Nacional Autónoma de México
– Fernando Abigail Galicia, Universidad Nacional Autónoma de México
– Javier Enriquez Mendoza, Universidad Nacional Autónoma de México

United States
– Henry Blanchette, Reed College

Argentina
– Andrés Ezequiel Viso, Universidad de Buenos Aires
– Christian Roldán, Universidad de Buenos Aires
– Cristian Sottile, Universidad Nacional de La Plata y Quilmes
– Francisco Carlos Trucco, Universidad Nacional de Córdoba
– Guido Martínez, Universidad Nacional de Rosario
– Ignacio Tiraboschi, Universidad Nacional de Córdoba
– Malena Ivnisky, Universidad de Buenos Aires
– Matías Steinberg, Universidad Nacional de Córdoba
– Rafael Romero, Universidad de Buenos Aires
– Santiago Arranz Olmos, Universidad Nacional de Córdoba

Bolivia
– Carlos Gómez, Industry

Brazil
– Leonardo Vieira dos Santos Reis, Universidade Federal de Juiz de Fora
– Rafael Castro Gonçalves Silva, Universidade do Estado de Santa Catarina
– Rodrigo Geraldo Ribeiro, Universidade Federal de Ouro Preto

Chile
– Bernardo Subercaseaux, Universidad de Chile
– Bruno García Agapito da Veiga, Universidad de Chile
– Damián Arquez Trigo, Universidad de Chile
– Daniela Campos, Universidad de Chile
– Dario Palma Carrasco, Universidad de Chile
– Elizabeth Labrada Deniz, Universidad de Chile
– Federico Olmedo, Universidad de Chile
– Kai Klingenberg, Inria Chile
– Matías Toro, Universidad de Chile
– Raimil Cruz, Universidad de Chile
– Ricardo Honorato-Zimmer, Universidad de Valparaiso
– Robinson Alexis Castro Fernández, Universidad de Chile Chile
– Tomás Díaz, Instituto Milenio Fundamentos de los Datos

Uruguay
– Damián Ferencz, Universidad de la República
– Juan García Garland, Universidad de la República