@InProceedings{Kahl-2011c,
  author = 	 {Wolfram Kahl},
  title = {The Teaching Tool 
    {{\sf {C{\scriptsize{\sf ALC}}C{\scriptsize{\sf HECK}}}}}:
    A Proof-Checker for Gries and Schneider's
    ``Logical Approach to Discrete Math''},
  crossref =  {CPP2011},
  SpringerURL = {http://www.springerlink.com/content/k05455151065817m},
  DOI = {10.1007/978-3-642-25379-9_17},
  pages = 	 {216--230},
  abstract = {Students following a first-year course
      based on Gries and Schneider's LADM textbook
      had frequently been asking:
      ``How can I know whether my solution is good?''

      We now report on the development of a proof-checker
      designed to answer exactly that question,
      while intentionally not helping to find the solutions in the first place.
      \CalcCheck{} provides detailed feedback to \LaTeX{}-formatted calculational
      proofs,
      and thus helps students to develop confidence in their
      own skills in ``rigorous mathematical writing''.

      Gries and Schneider's book emphasises rigorous development
      of mathematical results,
      while striking one particular compromise between full formality
      and customary, more informal, mathematical practises,
      and thus teaches aspects of both.
      This is one source of several unusual requirements
      for a mechanised proof-checker;
      other interesting aspects arise 
      from details of their notational conventions.}
}

@Proceedings{CPP2011,
  title =         {{Certified Programs and Proofs,
        First International Conference, CPP 2011,
        Kenting, Taiwan, December 7-9, 2011. Proceedings}},
  booktitle =     {Certified Programs and Proofs, {CPP 2011}},
  lncsbooktitle = {CPP 2011},
  year =          2011,
  editor =    {J.-P. Jouannaud and Z. Shao},
  volume =    7086,
  DOI = {10.1007/978-3-642-25379-9},
  SpringerURL = {http://www.springerlink.com/content/k852777819kq/},
  series =    LNCS,
  publisher = Springer
}