Content

• News
• General Information
• Course Material
• Exercises
• Exams
• Schedule
• Old News

News

• 05/25/2011: I have put a goals of the exercises page in the wiki, so you can check if you meet them yet or have to put in additional effort.
• 05/04/2011: We created a wiki for you to look up information and contribute actively!

General Information

• Semester: SS 2011
• Lecturer: Prof. Dr. K. Madlener
• Teaching Assistant: Patrick Michel
• KIS-Entries for the lecture and the exercises.
• Dates and Rooms:
  
  • Mondays, Wednesdays, and Thursdays from 11:45 to 13:15.
  • The lecture room was 48-462.
  • The exercise meetings were in the SCI terminal room in 32-411.
  • The schedule was moved to the end of the site.

Course Material

• These are the slides per chapter. A combined set of slides is also available and will be updated regularly, as new chapters are added: svhol.pdf
  The combined set might contain corrections and updates to slides, which are not (yet) reflected in the chapter files.
  
  

  Content	Material
  0. Organisation and Overview	svhol1.pdf
  1. Functional Programming	ML_Survey.pdf
  2. Functional Programming:Isabelle	svhol2.pdf
  3. HOL:Foundations	svhol3.pdf
  4. Proof System of Isabelle/HOL	svhol4.pdf
  5. Sets, Functions, Relations, and Fixpoints	svhol5.pdf
  6. Verifying Functions	svhol6.pdf
  7. Application: Inductively Defined Sets	svhol7.pdf
  8. Application: Programming Language Semantics	svhol8.pdf
  9. Application: Verification of distributed systems	svhol9.pdf
  10. Conclusions: Overall structure	svhol10.pdf

  
  
• Acknowledgement: We thank
  • Dr. Jens Brandt for the first version of the slides.
  • Prof. Poetzsch-Heffter for his course material.
  • Prof. Slind for the introductory remarks on HOL.
  • Prof. Basin, Dr. Brucker, Dr. Smaus, Prof. Wolff, and the MMISS-project for the slides on HOL.
  • Prof. Nipkow for the slides on Isabelle/HOL.
• The newest version of the tutorial "Isabelle/HOL --- A Proof Assistant for Higher-Order Logic" by Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel (originally published by Springer as LNCS volume 2283) can be found at http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf.
• The following links refer to pdf-versions of the theory Main provided by Isabelle/HOL:
  • http://isabelle.in.tum.de/dist/library/HOL/document.pdf contains the complete theory
  • http://isabelle.in.tum.de/dist/Isabelle/doc/main.pdf contains a summary

Exercises

• The exercises to the course make up half of the weekly meetings. As with the lecture itself, participation is not mandatory, yet the content is relevant for the exams.
• The exercise sheets are available online. Please at least prepare all the parts of the sheet, which are marked accordingly. We will then work on the remaining parts within the next exercise meeting.
• The exercise meetings are in the SCI terminal room in 32-411.
• We will organize the exercises using small groups, which collect the solutions and moderate the exercises. Please sign up for these groups in the PAS system.
• Please send your solutions to me in a timely manner, so the organizing group has time to view it and prepare. You can also give me solutions as hard copy, so I can scan them and send them to the group.
  
  

  Sheets
  No.	PDF	Date	Prepare	Remarks
  1	Sheet1.pdf	04/18/2011	04/27/2011
  2	Sheet2.pdf	04/27/2011	05/04/2011
  3	Sheet3.pdf	05/03/2011	05/11/2011	Exercise 2 is meant to be solved just by using type_synonym, not the typedef construct you have seen in the lecture! We will work with the latter on another exercise sheet. Altogether this should make the exercise fairly easy and the solution quite short.
  4	Sheet4.pdf	05/10/2011	05/18/2011
  5	Sheet5.pdf	05/17/2011	05/26/2011
  6	Sheet6.pdf	05/26/2011	06/08/2011
  7	Sheet7.pdf	06/22/2011	-
  8	Sheet8.pdf	07/04/2011	-
  9	Sheet9.pdf	07/12/2011	-
  10	Sheet10.pdf	07/20/2011	-

  
  

  Additional Material
  No.	File	Description
  1	Lecture.sml	The SML File I wrote in the lecture as introduction.
  	Types.sml	The SML File I wrote in the lecture for the stack example.
  	Prover.sml	An additional SML File containing the prover from the slides, in essence.
  2	Calculi Introduction	The material presented by the moderating group of Sheet 1.
  	Hilbert Calculus Exercise
  	Natural Deduction Exercise
  3	Cheat Sheet	A PDF document with useful hints to Isabelle/HOL and the proof general.
  	Cheat Sheet	A small webpage with some basics about Isabelle/HOL
  4	Hilbert.thy	A template for the translation of the proofs in the Hilbert calculus.
  5	ToyList.thy	Additional material used in the lecture.
  	BinaryTree.thy
  6	Lecture.thy	The theory file used in the lecture (05/09/2011).
  7	DemoSetsFunRel.thy	Demo material used in the lecture and for you to work with.
  	Sets.thy
  8	Mynat.thy	Demo material from the lecture.
  	gcd.thy
  9	Universe.thy	The material needed for Sheet 7.
  	QSort.thy
  	EQSort.thy
  	MSort.thy
  10	Elevator.thy	The theory file used in the lecture (06/27/2011).
  11	MyWhileLang.thy	The theory file used in the lecture (07/04/2011).
  12	While.thy	The material needed for Sheet 9.
  13	MyHoare.thy	The theory file used in the lecture.
  14	Link	Overview over available provers.

Exams

• We have fixed two dates for the oral exams:
  • Thursday, Aug 4, 2011 (08/04/2011)
  • Thursday, Oct 6, 2011 (10/06/2011)
  To register for an examination, please send an email to the professor (and put the TA on CC). Please refer to the General Information section for contact information.
• If you have any questions please don't hesitate to ask.

Schedule

• The lecture and exercises were scheduled as following:
  
  

  Schedule
  Week	Date	Event	Group
  1	04/18/2011 (Monday)	48-462 (lecture)
  	04/20/2011 (Wednesday)	48-462 (exercise/lecture)
  	04/21/2011 (Thursday)	48-462 (lecture)
  2	04/27/2011 (Wednesday)	32-411 (exercise)	1
  	04/28/2011 (Thursday)	48-462 (lecture)
  	04/29/2011 (Friday, 11:45)	32-411 (exercise)	-
  3	05/02/2011 (Monday)	48-462 (lecture)
  	05/04/2011 (Wednesday)	32-411 (exercise)	2
  	05/05/2011 (Thursday)	48-462 (lecture)
  4	05/09/2011 (Monday)	48-462 (lecture)
  	05/11/2011 (Wednesday)	32-411 (exercise)	4
  	05/12/2011 (Thursday)	32-411 (exercise)	-
  5	05/16/2011 (Monday)	48-462 (lecture)
  	05/18/2011 (Wednesday)	32-411 (exercise)	3
  	05/19/2011 (Thursday)	48-462 (lecture)
  6	05/23/2011 (Monday)	48-462 (lecture)
  	05/25/2011 (Wednesday)	32-411 (exercise)	-
  	05/26/2011 (Thursday)	32-411 (exercise)	5
  7	05/30/2011 (Monday)	48-462 (lecture)
  	06/01/2011 (Wednesday)	32-411 (exercise)	-
  	06/03/2011 (Friday, 11:45)	32-411 (lecture) !
  8	06/06/2011 (Monday)	48-462 (lecture)
  	06/08/2011 (Wednesday)	32-411 (exercise)	1
  	06/09/2011 (Thursday)	32-411 (exercise)	-
  Pentecost
  9	06/20/2011 (Monday)	48-462 (lecture)
  	06/22/2011 (Wednesday)	32-411 (exercise)
  	06/24/2011 (Friday, 11:45)	32-411 (exercise)
  10	06/27/2011 (Monday)	48-462 (lecture)
  	06/29/2011 (Wednesday)	32-411 (exercise)
  	06/30/2011 (Thursday)	48-462 (lecture)
  11	07/04/2011 (Monday)	48-462 (lecture)
  	07/06/2011 (Wednesday)	32-411 (exercise)
  	07/07/2011 (Thursday)	32-411 (exercise)
  12	07/11/2011 (Monday)	48-462 (lecture)
  	07/13/2011 (Wednesday)	32-411 (exercise)
  	07/14/2011 (Thursday)	32-411 (exercise)
  13	07/18/2011 (Monday)	48-462 (lecture)
  	07/20/2011 (Wednesday)	32-411 (exercise)
  	07/21/2011 (Thursday)	48-462 (lecture)
  end of the lecture (exams)

Old News

• 09/27/2011: Because of the large demand for appointments to ask questions about the content of the lecture, I have scheduled a meeting with everyone who is interested on Friday, 30. September, 10 am, at my (the TA's) office. You will be able to ask questions for about two hours and we will discuss them in the group.
• 07/29/2011: The slides for the last chapter are now online, as is the MyHoare theory and the link to the page listing available provers.
• 07/27/2011: <snip> ... </snip> Long story short; Yesterday we had a nice meeting at Bremerhof :-). Good luck with the exams, everyone, and feel free to ask questions (and contribute to the wiki)!
• 07/04/2011: We updated the examination information with two dates for which you can register.
• 07/25/2011: At the moment it looks like we will meet this Tuesday. So if you want to participate in the event and haven't voted yet, please do so, no matter if you prefer this or next week!
• 07/21/2011: We would like to get together one more time, in an informal setting at the Bremerhof. If you like to participate and drink with us, please vote for a date which suits you :-) We would like to fix the date next Monday or Tuesday the latest.
• 07/18/2011: New slides for Chapter 9 are now online.
• 07/04/2011: New slides for Chapter 8 are online, as well as the theory used in the lecture. The schedule was also updated.
• 06/27/2011: New slides for Chapter 7 are online, as well as the elevator theory introduced there.
• 06/22/2011: Sheet 7 is now online and will be worked on on Friday.
• 06/20/2011: New slides for Chapter 6 and two additional demos are now online.
• 05/27/2011: Chapter 5 of the slides was updated and the additional material table now contains two more demos for you to work with and which were used in the lectures.
• 05/23/2011: New slides for Chapter 5 are online, the slides for Chapter 4 might have changed (updated). The combined pdf always contains all updates and changes made to slides.
• 05/26/2011: Exercise Sheet 6 is now online and needs a moderating group! There is plenty of time to prepare it, so I would be glad if some group volunteered!
• 05/18/2011: We decided to delay the next exercise sheet 5 for one exercise, i.e. we will start with it on Thursday, the 26. Consequently the Wednesday in week 7 will be to finish with this sheet and there will be no new sheet for this day. On next Wednesday we will therefore continue with Sheet 4, the typedefs and the rule applications. You still have to prepare Sheet 5 for next week, send in your solutions and continue with solving Sheet 4.
• 05/17/2011: The schedule was updated and Sheet 5 is now online.
• 05/13/2011: New slides are online and the schedule was updated.
• 05/10/2011: Please turn in your solutions for Sheet 3, I didn't get any solutions yet!
• 05/10/2011: Exercise Sheet 4 is now online and the theory file used in the lecture is available under Additional Material.
• 05/03/2011: Exercise Sheet 3 is now online.
• 05/02/2011: The slides for Chapter 3 are now online, the Additional Material table also contains the theories from the lecture. The schedule was updated.
• 05/02/2011: We will have a moderating group for the next exercise after all, so please send any solutions for Sheet 2 to me. If you are a member of the moderating group, please contact me to let me know which PAS group you correspond to, so I can send you the solutions.
• 04/27/2011: Updated the schedule and put the second exercise sheet online.
• 04/26/2011: Please send your solutions to me in a timely manner, so the organizing group has time to view it and prepare. You can also give me solutions as hard copy, so I can scan them and send them to the group. As the first exercise is tomorrow, it would be nice to receive at least some solutions today, the earlier the better.
• 04/21/2011: Please register for the exercises using the PAS system. There are currently nine groups, which do not differ in any way, they are just to create the small working groups we talked about.
• 04/21/2011: I have created a poll on Doodle to schedule the second exercise date next week, since Monday is a holiday. The options I put in are directly before and after the first exercise and all slots on Friday.
• 04/21/2011: New slides are online and we have added the planned schedule.
• 04/18/2011: On Wednesday (04/20/2011) we will meet in 48-462 for the next lecture/exercise! The first exercise sheet is also online now.
• 04/13/2011: The first slides are online.