The Hitchhiker’s Guide to Logical Verification by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg. This text is freely available in PDF format.
Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community. This text is freely available from HTML format.
All students are expected to attend classes in which they are enrolled regularly and punctually. Failure to do so may jeopardize a student’s scholastic standing and may lead to suspension from the College or University.
The student is responsible for making arrangements satisfactory to the instructor regarding absences including prior notification of planned absences, providing documentation if needed, and making up of examinations and work as required. For other emergency absences, the student shall submit excuses for class absences to the appropriate instructor within three class days following the student’s return to their respective class.
As noted above, students are obligated to complete all assigned work promptly, to attend class regularly, and to participate in whatever class discussion may occur. Any behavior that interferes with the ability of other students to learn is unacceptable. If any of these become an issue, you will be asked to leave class for the day.
Your phone should be on silent and put away during class. Headphones should also be put away during class. Texting and browsing social media during class is rude and disrespectful. Please refrain from using your phone during class unless explicitly stated otherwise. If you are caught with a cell phone on your desk, in your lap, or anywhere in view while taking a quiz or exam, it will be treated as a case of academic dishonesty. Smart watches are also prohibited during exams; please put them away during those times.
Late work will not be accepted. Students who cannot submit work due to a University-related activity requiring an absence from class must arrange for work to be submitted before leaving.
Make-up opportunities will only be granted in cases of documented emergencies or university-approved absences (e.g., illness, family emergencies, or official university activities). Except in extraordinary circumstances, students must notify the instructor before the missed deadline or class. Students who need to make up work due to a University-related activity requiring an absence from class must arrange for work to be completed before leaving.
Any suspected case of academic dishonesty will be reported. If it is determined that academic misconduct has occurred, the student will receive a grade of F for the course and may be dismised from the University.
