| Machine Problems for Spring 2012 |
Isabelle is available on the EWS Linux machines. You may run it
remotely using ssh -Y. To use Isabelle on remotely
remlnx.ews.illinois.edu execute:
~cs576/isabelle emacs
|
|---|
Homeworks will be in the form of theory files to be completed. A
completed theory file should have no occurrences of "sorry".
Homeworks should be submitted to me by use of the handin>
program on the EWS linux machines. For example to submit MP0 from
remlnx.ews.illinois.edu execute:
~cs576/handin -s mp0
|
|---|
|
The MPs for the semester have been posted, but they are subject to
modification, or even complete replacement, until officially asigned. In particular, unassigned MPs may be for a previous version of Isabelle.
|
|---|
| MP |
Date Assigned |
Due Date |
Solution |
| MP 0 (mp0.thy) |
Tuesday, 17 January 2012 |
Thursday, 19 January 2012, 12:01pm |
MP 0 Solutions given (mp0-sol.thy),
| |
| MP 1 (mp1.thy) |
Thursday, 19 January 2012 |
Thursday, 26 January 2012, 11:59pm |
MP 1 Solution(mp1-sol.thy),
Isar style(mp1-isar-sol.thy) |
| MP 2 (mp2.thy) |
Thursday, 26 January 2012 |
Thursday, 2 February 2012, 11:59pm |
MP 2 Solution(mp2-sol.thy),
Isar style(mp2-isar-sol.thy) |
| MP 3 (mp3.thy) |
Thursday, 2 February 2012 |
Thursday, 9 February 2012, 11:59pm |
MP 3 Solution(mp3-sol.thy)
Isar style(mp3-isar-sol.thy) |
| MP 4 (mp4.thy) |
Thursday, 9 February 2012 |
Thursday, 16 February 2012, 11:59pm |
MP 4 Solution(mp4-sol.thy) |
| MP 5 (mp5.thy) |
Thursday, 16 February 2012 |
informal proof, Thursday 23 February Thursday,
mp5.thy, 1 March 2012, 11:59pm |
|
| MP 6 (mp6.thy) |
Thursday, 1 March 2012 |
Thursday, 8 March 2012, 11:59pm |
|
|
|
