WikiDoc 
CoqModeCoq is is a proof assistant for computer assisted verification of mathematical proofs. The home page is http://coq.inria.fr (where an easytoinstall OSX version can found). Proofs are written in the specialpurpose lambdacalculuslike language 'gallina'. coqtop is the top level command interpreter for coq. A Coq mode for Alpha is in development, featuring a coq console for interaction with coqtop. The most interesting aspect of this mode is perhaps the stepconsole functionality (described on the page Pipes.StepConsoles). It also illustrates the strictConsole package (included): a mechanism that prevents anything from being typed above the prompt in a shelllike window. Coq mode, which requires AlphaTcl from CVS HEAD newer than 20050308, can be downloaded from http://mat.uab.es/~kock/alphatcl/coq.tar.gz . Included is an example file giving a formal proof of the commutativity of 2monoids (the EckmannHilton argument). You can play with the step functionality by pressing enter in this file. Finally there is included a transcript of the console window after stepping through the proof, in case you haven't got Coq installed but want to have a look at what this is all about. 
Edit 
History 
Print 
Recent Changes 
Search
Page last modified on January 23, 2006, at 02:01 PM

Hosted on 