CS 477: Formal Software Development Methods
News for Spring 2018
  • 2/9/18 - There is a disagreement for problem 2 between the statement in the pdf file and the statement in the thy file. In class I said that the pdf would be the ultimate authority, but I see that several students have already finished and did the problem that was in the thy file. Therefore, I will allow everyone to do either version. The one in the thy is a little shorter. - ELG
  • 1/29/18 - I am changing the extra credit problem to only be one direction of what I originally asked. You only need to show:

    For all propositions P, if there exists a proof of the sequent { }⊢ P in the sequent encoding of the Natural Deduction system, then there exists a fully discharged proof of P in the Natural Deduction system.

    The other direction requires something call weakening for the sequent proofs, which requires a proof in its own right. - ELG
  • 1/21/18 - Welcome to CS477, Spring 2018. This page will be the main bulletin board for the course, and hence is always under construction. Please check it frequently. - ELG
  • 1/21/13 - Caution: All the webpages for this course are currently under conversion. I have copied then shamelessly from my webpages for cs421, and revised them but there may still be cs421 detritus in them. Please point out any oddities and I will fix them (or explain them). - ELG
    Contacting Staff
    Submitting Assignments
    Regrade Policy

    Class Schedule
    Wed, Fri 9:30am - 10:45am
    1131 SC

    Elsa Gunter
    Email: egunter@illinois.edu
    Office: 2112 SC
    Phone: 265-6118
    Hours: Wed 1:30pm-2:30pm, Fri 11:00am - 11:50 pm
    Also by appointment