The Science of Deep Specification

Arrival and departure

The summer school will open with a three-day intensive course on the fundamentals of the Coq proof assistant, for participants who are new to Coq.

The main lectures take place during the weeks of July 17 and July 24.

July 13-15 (Thu-Sat) Coq intensive
July 17-21 Week 1 (Leroy, Pierce, Weirich, Zdancewic)
July 24-28 Week 2 (Appel, Chlipala, Kaashoek/Zeldovich, Shao)

The last lecture will end by 4PM on July 28th. For funded participants, dorm rooms have been reserved through the night of the 28th.

Participants in the Coq intensive should plan to arrive on Wednesday, July 12th. For those staying in the dorm, the check-in period will be from 6 to 8 PM; please try to arrive between those times. (If this is not possible, let us know and we can work out another arrangement.)

Students who are not participating in the Coq intensive should plan to arrive on Sunday, July 16th. Again, for those staying in the dorm, the check-in period will be from 6 to 8 PM; please try to arrive between those times.

Travel information

The nearest airport is Philadelphia International (PHL). Newark International (EWR) and Baltimore-Washington International (BWI) are within an easy train ride; the Amtrak 30th St. Station (PHL) is a few minutes' walk from Penn and Drexel. Alternatively, there are taxis ($35ish, with tip) and Uber/Lyft ($20ish).


There are two forms of housing for the summer school:


For DSSS17-funded participants, vouchers will be provided for breakfasts and dinners at Penn campus dining facilities. Lunches will be at participants' own expense; the Penn campus area hosts dozens of excellent and inexpensive lunch trucks.

Self-funded participants can eat at the same campus dining facilities. The cost is approximately $10 for breakfast and $15 for lunch or dinner. Meals can be purchased on the spot – no need to buy vouchers in advance.


We’ve set up three ways of exchanging information during the summer school:

  1. The mailing list for official announcements and questions of general nature. Every participant must subscribe to this mailing list. Participants are welcome to use the list for things that are of interest to everybody, but please keep the signal-to-noise ratio high.
  2. The Piazza group is especially for asking and answering questions about homework. Participants should have received an invitation by email. Participation is optional.
  3. The Slack team is for more ephemeral, real-time, potentially high-volume discussions. Participation is optional.

Wifi access

Guests to Penn campus can get access to the campus wifi network like this:

  1. Select the “AirPennNet-Guest” network
  2. Open a browser
  3. Review and accept the Acceptable Use Policy terms and conditions
  4. Enter a valid email address
  5. Click Submit

Eduroam is also available.

Further questions

Questions about the summer school should be directed to Benjamin Pierce.