University of Oregon

Oregon Programming Languages Summer School

Types, Semantics, and Logic

June 26-July 8, 2023

Jim's OPLSS Blog


I have nothing to say here, but I wrote the aside about the Stonewall riots a while ago, thinking I would probably have something to say today.


Your room and board plan includes breakfast (7AM-9AM), lunch (NOON-2PM) and dinner (5PM-8PM). I will try to predict other groups using the cafeteria at the same time as us, and make announcements at lecture. In general, the youth athletic camps break for lunch at noon and resume at 1PM, so normally, you will do better to go to lunch at 12:45 or so. Similarly, the kids are hungry after physical activities, so they tend to eat dinner at 5PM. It is better to eat dinner at 6PM or 7PM, like a normal person. The nutritional information about cafeteria foods is available at including information on specific food alergies.

The restrooms in the North end of the Law Center promenade are marked "male" and "female". There is no law in Oregon about how to assign gender identity. The restrooms nearer the lecture hall are marked "Urinals and Stalls" and "Only Stalls".

Recreation Center

While you are here, you can buy a pass to visit the Student Recreation Center. You can check out the facilities and hours online, or try purchasing a one-day pass at the campus location. Multiday passes require a UO Community Card.

Inter-Cultural Communication

For non-Americans, asking simple directions can be tricky. The points of reference that are valid in European cities are not the same in American cities. It is always better to ask me, or someone from Eugene, a specific question than a general one. For example, one year, a European woman said that Eugene natives act friendly, but they are really duplicitous. "How so?" I asked. "Well, every time I ask directions to downtown, they tell me how to get to the library." "Take the EMX to Eugene Station" "I don't want to go to the library. I want to go downtown." "Downtown is the library and the bus station and maybe Voodoo Doughnuts if you want to be really liberal in your definition." "I want to go to the section of town with lots of dancing." "Well, you'll never find that downtown unless you feel like dancing in the street while you eat a doughnut. Three blocks North of downtown is the barmuda triangle, but Taylors is just West of campus." Her cultural reference to "downtown" was not the Eugene understanding of the term. Thus, it is better to just say what you want, as in "I want to go dancing," and we will cheerfully tell you where to go.


Oregon is not a humid climate. If you are from the US interior Southwest, you may find it a bit humid, but if you are from anywhere East of the Rocky Mountains in the US, or some foreign places, you will find it very dry. This means that at night, there is a 30F or more drop in temperature. Because the usual school year runs from October to May, the dorms have heating, but no air conditioning. The typical pattern in Oregon is to open the windows when the sun goes down, but keep them closed in the heat of the day. (see the May 5 aside about hay fever)

While you are in Eugene, the weather will be hot, and the river will be cool, but don't go jumping into the river. The rivers here are fed by snow melt in the surrounding mountains. Therefore, the water is barely above freezing. People occasionally jump into the river to cool off, and their bodies are recovered downstream. Wading is refreshing, but do not jump into the water all of a sudden without acclamation.


There is no drinking alcohol allowed in public areas in Oregon (and specifically on the University of Oregon campus) unless you have OLCC licensed servers controlling access. Specifically, this means that you can drink in your dorm room, if the door is closed and the people in your room are all 21 years or older, (Supplying alcohol to people under 21 is illegal.) but you cannot drink in the public areas of the dorm. — One year, OPLSS participants had the idea to put beer bottles in the ice machine, and the 10 year olds in the building were stealing the beer to take to their rooms and drink.


Similarly, there is no smoking marijuana in public or supplying it to minors in any form. See section below for limitations on smoking, which include marijuana. Eugene's marijuana shops offer a large variety of edible products.


Oregon cities are largely non-smoking. Smoking includes tabacco, clove cigarettes, marajuana, and anything else that causes people in your vicinity to partake in the drug you are inhaling.

In Oregon, it is illegal to smoke inside a public building or within 20 feet of any building entrance, or on State owned lands, such as a beach or wilderness area. The city of Eugene does not allow smoking in city-owned places, such as parks or transit facilities. The University of Oregon is a Smoke and Tobacco Free University, which includes prohibiting vaping or smoking marijuana in your dorm room. Smoking by OPLSS participants who are not UO students results in a $30 fine. If you are staying at a hotel, it is probably smoke-free — ask the hotel. This means that you will be hard pressed to find anywhere to smoke conveniently. You can stand in the middle of some streets, waterways and railroad tracks on campus, and while it is not technically illegal to smoke there, it is strongly discouraged for safety reasons, and casual littering like leaving a cigarette butt in the street is illegal. In most places in Eugene, smoking does not include ecigs, but University of Oregon policy considers them a prohibited tobacco product. Chewing tabacco is similarly prohibited by the University, but not the city or the state; however, most restaurants, bars and taverns will not allow chewing tobacco, and spitting chewing tobacco in the street is the kind of casual littering that is illegal in Oregon. (Oregon invented returnable beer bottles in 1967 to cut down on casual littering.)

Therefore, if you are addicted to nicotine, in addition to the items listed on May 5, you should plan on bringing nicotine gum or patches..

The mailing address for you at OPLSS is:
your name
1710 East 15th Ave
Eugene OR 97403
Mail must be received at the mail room between June 24 and July 7, otherwise it will be returned as undeliverable

On the travel page, if you are going from the Portland airport to the Amtrak station, it suggests you take the MAX Red Line. Portland will be shutting down the MAX Red Line over the summer for repairs to the track. There will still be a shuttle service between the airport and the MAX Green Line train, but this is expected to add about 30 minutes to your travel time.

On the topics page, the Introduction to Coq description tells you to install Coq "version 8.16 or later," but the Verified Compilation description tells you to install CompCert, which is documented to work with earlier version of Coq. Prof. Blazy reports she uses version 8.16 and it works fine with CompCert, but when you perform the installation, you must add "-ignore-coq-version" to the documented configure script options. That way, you can install ConpCert on top of Coq version 8.16 as required by Dr. Paykin.

Sandrine Blazy's lecture has been updated with a link to CompCert. You should install it on your laptop. Please note that you will have to already have Coq and OCaml to install it. (See installation instructions on the CompCert website.)

We are staying in the Global Scholars Hall. I have updated the check-in and check-out sections of the travel information page. Your check-in instructions will vary depending on what time you will arrive.

Points of interest on the map:

The housing packages with OPLSS begin with check-in at 2PM on Sunday, June 25. Your first meal is dinner that day from 5-7:30PM. You can arrive any time that day. If you arrive early, just wait in the lounge of the building. After the housing office closes at 8PM, you can get your keys by calling the number on the door. I will post that number here, when I get it. Flights arriving anytime between 8AM Sunday to 2AM Monday are pretty normal for OPLSS.

Please remember to tell me when you will be arriving. (see the Travel page)

The housing packages with OPLSS end with check-out before Noon on Sunday, July 9. Your last meal is lunch at 11AM on Sunday. People sometimes book flights that leave during the last lecture on Saturday. I would suggest not doing this if you can avoid it. If your flight leaves on Monday, you will have to arrange a motel room, or a stay at the Eugene Hostel.

If you are thinking of driving a car to OPLSS, or renting a car when you get here, think again. The University of Oregon's general policy on driving to campus is "Who told you to do that?" During the school year, I would definitely tell you not to bring a car. During the summer, you may be able to find parking. If you insist on having a car, you can obtain a visitor parking permit from the UO Transportation Office . The "permit" is a virtual permit that allows a car with your license plate to park, and must be purchased each day.

The local hospital and the university have a bike share service. You can visit their website and set up an account. The rental bikes are distributed around Eugene, and you rent one by walking up to it and scanning the QR code with your phone. The bike will unlock for you. Your account is charged for the time you spend riding it until you lock it up again at your destination. The bikes do not come with a helmet, so please bring your own.

Access to computing resources on campus is governed by applicable US laws. In particular, US law says that sharing copyrighted content over the Internet is illegal, and the copyright holder is entitled to huge damages from the University of Oregon, if they allow it. Therefore, the University of Oregon has incentives to disable your access if you are doing something illegal.

UO policy also requires you have the latest security updates to your OS. Sometimes, the network will be able to detect if you are accessing with a machine that does not have required updates. So, please be sure your laptop is up-to-date security-wise before coming to campus.

If you notice that your connections go dead after a few minutes, this is not because the UO connections don't work; rather, it is because you have been disallowed from network access. Please talk to me about re-establishing the network access for your MAC address.

Health Care

In the US, if you need urgent assistance call 911. The emergency operator can connect you with emergency medical service providers, the fire department or the police in any jurisdiction in the US. This should work on cell phones. For non-threatening situations, you can use University Oregon emergency contacts.

If you need health care for non-life threatening conditions, you should go to Bestmed Urgent Care which is west along 13th street past the end of campus, three blocks to Patterson. It is on the SW corner. It is open 8AM to 8PM every day. You should expect to pay a hundred or more dollars if you do not have insurance.

If you need major medical treatment, you should go to the Emergency Room at PeaceHealth, Sacred Heart, University District campus which is west along 13th street past the other end of campus, two blocks to Hillyard. It is on the NE corner. It is always open. You should expect to pay several thousand dollars if you do not have insurance. If you have to be transported by ambulance, that will be several thousand dollars more. (I pay $35 every year and get free ambulance rides — the US system is geared toward insurance, not pay-as-you-go.) For people not familiar with US health care, they will ask for your address. You should give them your home address in your country because you will receive several bills to that address as much as three months after the services were provided.

The Emergency Room at Sacred Heart can treat everything that Nova Health can treat, but at much higher cost. Even if you have insurance that covers medical expenses, emergency room care can be very confusing if you are not used to American health care. After a trip to the emergency room, you can expect between five and ten separate bills from separate entities: the hospital itself, and every person who treated you, or consulted in your treatment, some of whom you may not have met. US law says that Sacred Heart must treat you and determine costs and payment later. Nova Health, on the other hand, will tell you all the costs, but will either expect you to provide your insurance information, or pay before receiving treatment.

If you are from another industrialized country, you will find the US Health Care system is much more expensive and not as good as what you expect (unless you are having a heart attack), but this is where you are, so you need to use what is available in an emergency. If you are not living in the US, you should obtain prior paperwork from your country to cover medical expenses while in the US.

On the topics page, Stephanie Weirich has included a link to the her pi-forall resources. In particular, before OPLSS, you should install ghcup for Haskell, vscode + LSP for editing, and pi-forall itself available from her guide to getting ready for the lectures.

Also, on the schedule are sessions Coq Lab on June 26 and June 27. If you haven't already, you should install Coq.

The website says you must pay your registration by the middle of May to hold your place at OPLSS. Also you must arrange or cancel your housing by the middle of May or be liable for the cost. If you have a fellowship and do not cancel before the middle of May, you will have to pay for cost if you do not attend, because our sponsors only pay for costs incurred by people who attend.

During OPLSS, you can use the UO guest wireless network or the eduroam wireless network. To use eduroam, your institution must be a member. Please consult your campus network administrator before arriving at OPLSS.

UO guest and eduroam will work well in your dorm or on other places on campus; however, the classroom is configured to have fewer than a dozen guests and fewer than a dozen eduroam users when classes are in session. So, you will have limited bandwidth. I suggest you take the following steps:

  • During lectures, use only text-based services on your laptop.
  • Download any software used by the lecturer before attending the lecture. Details of software used in the lectures are contained on the topics page under the entry for each lecturer.

Please don't pay for things that don't appear on your invoice! If you want to change your accomodations, please email me and I will send you a corrected invoice which you can pay. Make sure that the amount you pay is the total that says "pay this amount" It looks very bad to auditors if you pay more money than your invoice shows. If you have extra money lying around, book a trip to Trinidad and Tobago, but do not send it to me unless I have sent you an invoice that indicates that amount on the "Total Due" line.

Things to bring to the summer school:
  • A laptop
  • Soap or shower gel, shampoo, toothpaste and other personal grooming items.
  • The dorm does not have hair dryers or irons. I think of these as "personal grooming items,". Hot plates and other cooking appliances are not allowed in your dorm room.
  • Typically, I tell everyone to bring allergy medication. The main agricultural products in the Willamette Valley are grass seed and mint, so if you are allergic to grass pollen, expect to feel the effects while you are here. Typically, the grass pollen count is worst in June, with the level tapering off as summer progresses. Some students travelling to OPLSS experience pollen allergies for the first time. You can see a complete pollen report at, zip code: 97403 (pay attention to the grass number). Pseudofed is a prescription drug in Oregon, so if you intend to purchase it here, either bring a prescription, or use one of the better, non-prescription alternatives.

I suggest you not bring your own sheets and towels since housekeeping will probably throw them in with the hall's linen when they change your room linens. In the past, this has lead to much consternation, especially if your linens are white, or slightly off-white as you look through the campus collection of laundry trying to find your sheets. If you do need to bring your own sheets, I suggest you put a sign on your door asking that your linens not be laundered. Also, talk to me so I will talk to the housekeeping staff.

I thought this would be obvious: the dorms have laundry facilities . Currently, laundry cost $1.50 and dryers are free. This price is subject to change when the contract is renewed at the beginning of summer, but should not be drastically different.

If you have a housing package, the meals will be served at the Cafeteria. The hours are:

  • Breakfast 7:00 AM - 10:00 AM
  • Lunch 11:00 AM - 2:00 PM
  • Dinner 5:00 PM - 8:00 PM
If you are not staying in the OPLSS housing, you can pay at the cafeteria door and eat with the other participants. The menu (hours will change during summer) and the item labels in the serving area contain markings for problematic food ingredients, including milk, eggs, fish, shellfish, tree nuts, peanuts, wheat, soybeans and sesame seeds.

Some common concerns:
Food Allergies
Vegetarian/Vegan/Raw Foodist
If you are vegan or vegetarian, there should be no problem finding adequate hot and cold food in the cafeteria. If you are raw foodist, there is an extensive salad bar. There is also a large selection of fresh and once frozen fruit, although some frozen fruits may have been blanched (heated briefly) before being frozen.
I do not know of any halal butchers in Eugene, and the cafeteria does not order halal meat. In general, my Muslim friends find plenty to eat at the cafeteria, by sticking to the vegetarian offerings.
Kosher is tricky. This surprised me since I know many Jews in town. Talking to my friends and the Jewish Student Union and Hillel and several Rabbis, it seems to come down to "if you live in Eugene, you have to make compromises." It is certainly possible to observe a Jewish-American, not-very-strict, kind-of-kosher, by abstaining from certain foods. In the cafeteria, asking "Is it kosher" is probably not as good an idea as asking for the ingredients, which the chef will be happy to share with you. Anyway, the answer to "Is it kosher?" is always no, since the cooking utensils and serving vessels are not kosher.
Since the meat in the cafeteria is neither expressly halal nor kosher, it is unlikely to be Kutha, but American butchery practice is not guaranteed to be strictly Jhatka either. Chickens are often killed with much suffering, for example, having their feathers removed prior to death. Cows and pigs can suffer as a result of unintentional mechanical failures. If you have strong ethical beliefs, you might want stick to the vegetarian options. (This is a general observation about US meat production. Our facilities maintain best practices within the US system.)
Free-Roam/Cage-Free Livestock
Since US law does not specify what it means to raise livestock cage-free, and the University does not have resources to investigate the source of animal products past the USDA oversight at the packing plant, asking for cage-free animal products would just be an invitation for suppliers to lie. Therefore, the dining hall cannot independently certify that any animal products were or were not produced in cage-free environments.

Happy May Day!

Oregon was the first US state to create a day honoring labor, although it was in June. There are links on the Venue page about the other great May Day tradition: Morris Dancing.

Acceptance has been established and grant funding has been allocated. You should have received a letter of invitation and an invoice from me. The letter of invitation has specific language for the US State Department during your visa interview, and specific language for the US Customs and Border Protection officers. Whether you go for a visa interview or obtain clearance through the Electronic System for Travel Authorization, you should have the letter of invitation ready at the border, and pay attention to my March 15 remarks about what not to say during a visa interview and at the border. You should also be ready for the coronavirus vaccine document requirements at the border.

To be clear: Housing is arranged through me. Going to the credit card website and paying for some kind of housing does not guarentee that kind of housing is available. You have housing reserved for you when I tell you I have reserved housing for you. (I will send you a new invoice with the new housing listed.) Similarly, not paying for housing does not cancel the housing I have reserved for you. Telling me to cancel your housing will cancel your housing.

Also, your registration charge is determined by me and listed on your invoice. When you go to the payment site, you need to pay the amount of money shown on your invoice. Do not pay for things that add up to more than your invoice shows you owe. As stated on the payment site, I cannot issue refunds.

By default, I will assume you want a shared room in the dorm. Based on capacity, we have a very limited number of single rooms available. You should let me know if you want a single room. Please let me know if you have mobility problems, although the dorm has an elevator, and the lecture hall is wheelchair accessible.

If you have a housing package for a shared room, and you know who you want as a roommate, please let me know by May 15th. I would encourage you not to do this. One of the purposes of OPLSS is to meet people in the field. When putting together the room roster, I try to put Americans with non-Americans, East Coast people with West Coast people, etc, to make sure that you are meeting people you would not otherwise know. If you ask me to put you in a room with your lab partner, I will do that, but you are missing out on part of the point of OPLSS. You already talk about PL research with your lab partner; this should be an opportunity to talk about PL research with someone else. Also, using a sophisticated algorithm, I put people from the same school in adjacent rooms, so it's not like you won't see the people you know.

This year, we will be in the Global Scholars Hall. The room layout for the dorm is Global Scholars Hall Double with sink. (You have to scroll down, the video is whitewashed, and the room is "lived in", but that is the only layout I have.) There is one communal bathroom for women and one for men. The showers have a small, private disrobing area next to the private shower, and the toilets are in individual metal privacy stalls.

In the past, very few participants have chosen to stay elsewhere during OPLSS. The dorms are not deluxe accommodations, but there is usually lots of discussion that goes on in the dorm, and participants who stay off-campus have felt isolated from this. However, if you want a hotel room near campus, here are a few options that are within a couple of blocks of the lecture hall.

There are many outdoor activities to do in Eugene. Within a 30 minute walk from the dorms are

Here is what should happen if you submit a Registration:
  • A webpage should show your registration was accepted and the details you just submitted. Please check the email address to make sure it is correct. If you submit a registration with a typo in the email address, I have no way to reach you. If you did make a typo in the email field, you should immediately email with the correction.
  • You should receive an email confirmation of your registration.
  • If you are applying for a grant, when we receive the required letter of recommendation, you will receive an email acknowledging the letter has been received.
  • About 10 days after the deadline, you will receive an email indicating your acceptance into the program. At that time, I will give you options for housing. You will only need to respond if you do not aagree with the housing I am offering you. If you do not respond, I will take that as you agreeing to that housing. When I have notified everyone of their acceptance, I will post a note on this website that I have done so. If you did not get an email from me, you should send an email to asking about your status, as I have probably misplaced your application.
  • If you are applying for a grant, it takes us longer to decide how the grant money is allocated. At some point, you will receive another email stating your grant status. When I have notified everyone of their grant status, I will post a note on this website that I have done so. If you did not get an email from me, you should send an email to asking about your grant status, as I have probably misplaced your grant application.
  • Sometime before May 19, you will need to pay your (non-refundable) registration and tell me whether you want a dormitory room. You do not need to pay for your room and board at that time, but I must tell the housing authority how many rooms we will require. OPLSS will be required to pay this amount, so either cancel by this date or you will be liable for the housing charge, whether or not you use it.
You should see as you arrange travel, that it is usually much cheaper to fly to Portland and then take a train to Eugene. The cost of a train from Portland to Eugene is approximately the same as the cost of a taxi from the Eugene airport to campus. If you are sharing the taxi, of course it will be cheaper for you, but you should find that although it takes a few extra hours to fly to Portland and take a train down, it will save you money.

Address for Visa Documents

When you get here, the building you will be staying in is:

1710 East 15th Avenue
Eugene OR  97403

However, do not send mail to that address. Mail addressed to university buildings (as opposed to departments) is returned as undeliverable. There is no phone number at the dorm, so you will have to use your own phone while you are here.

The contact information for visa applications is

Zena Ariola
University of Oregon
Department of Computer and Information Science
1477 E. 13th Avenue
Eugene OR  97403

It is never too early to work on obtaining travel papers to the US. The following are the guidelines I have offered successfully in the past.

For non-citizens of the US, you will need the following:
  • Travel papers to leave your country

    Most governments do not care if you leave their country, but you should check whether your government requires you to file any papers.

  • Travel papers to enter the United States

    Most governments do care if you enter their country, and the US is no exception. The US has a Visa Waiver Program with many countries. The Visa Waiver Program does not apply to all citizens of Visa Waiver Program countries.

    OPLSS is a Conference, not a Course of Study
    You are coming here on business to attend a scientific conference. OPLSS does not grant academic credit. Although OPLSS takes place on a university campus, it is not a course of study. You need to be clear that you are looking for a B1 business visa. Do not under any circumstances say or agree that you need a student visa. Once you say that you want a student visa or that you want to "study in the US", you will never be allowed to come to the US unless you have been accepted into a US degree-granting program.

    It is illegal for us to issue you an I-20 or any other SEVIS document, because you will receive no academic credit from the University of Oregon. These are only required for a student visa. If you are asked for these documents, be very clear that you want a B-1 visa. You will not be able to attend OPLSS on a student visa. If some other institution gave you a SEVIS document, and you will be using it to enter the US, please ask the entity that gave you the SEVIS document about your visa limitations. If necessary, direct them to this page for clarification.

    • Travel to the United States under the Visa Waiver Program
      • A Passport from your country of citizenship

        To enter the US, your country of citizenship must issue you a passport. Also, you may need your passport as identification while here.

      • Electronic pre-approval from the US

        When you fill out the electronic pre-approval form, and when questioned at the border, be clear that you are coming here for a scientific conference. Even though you will have to say University of Oregon and OPLSS, you want to emphasize that it is business purpose. Do not write school, study or student. Education purposes require a visa, even from visa waiver countries, and OPLSS cannot supply you with the required paperwork to obtain a student visa.

    • Travel to the United States without the Visa Waiver Program
      • A Passport from your country of citizenship

        To enter the US, your country of citizenship must issue you a passport Also, you may need your passport as identification while here.

      • A business visa from the US

        The decision to grant a visa is left up to the US ambassador to your country and there is no appeal, so be prepared. Talk to others from your country who have attended conferences in the US. Different Ambassadors require different levels of evidence. The University of Oregon has no influence with the US ambassador to your country. If your interview goes badly, and you are asked to do another interview, plan to bring more evidence. If you have no more evidence, then there is no point in another interview.

        Be prepared for your visa interview. Do not have anything sent directly to the embassy. Bring all materials with you to the interview. If some piece of evidence is not in English or not in the interviewer's language (the locally spoken language of that embassy), it must be translated by a certified translator. This means, if you are studying in a country which speaks a language other than your native language, documents from your country of citizenship must be translated. Here are the things you may need at your interview at the US embassy:

        • DS-160 Vias Application Form Complete the form online, but bring the confirmation page showing you completed the form and paid the $160 application fee
        • A valid passport issued by your country of citizenship
        • A photo (a copy of the photo you uploaded as part of the DS-160 application
        • Be prepared to submit all details of social media that you use.
        • Bank statements or other evidence that you will be able to pay all the costs of the trip.
        • Letters or printed social media showing you will not overstay your visa. This is very important. The interviewer must be assured that you are not a "risk to emigrate to the US". Evidence of this type can be communications with local relatives and friends showing they are dependent on your return and\or communications from your employer or academic advisor showing it would be more advantageous for you to remain in your country/program than relocate to the US.

          It is not useful to bring evidence of relatives or friends currently living in the US, as this indicates you may be a risk to emigrate to the US.

        I will issue a letter of invitation which you may also take to your visa interview, but it is not requried, and in general, the interviewer will not want to see it.

      Remember that neither electronic pre-approval nor a visa guarantee that you are actually allowed in the US. On the day you arrive, a US boarder guard will decide whether you are allowed in the US. For that interview, the invitation letter I send may be useful. On the other hand, this is where a participant was interogated for hours because she used the word "school." Be careful which words you use at the border. Remember, you are here to attend a scientific conference on computer science, not to attend a school of any kind.

  • Travel papers to return to your country

    Before you leave your country, make sure you have any papers necessary to return to your country, probably, a passport.

Here, I will be posting updates on registration deadlines, when you should expect to be notified, how to get here, and what to bring, etc.

If you apply (with a recommendation, if required) before April 3, you should hear back from us by April 10. If not, please send me ( an email asking what happened to your application.

© University of Oregon, All rights reserved