Logiweb

The Logiweb system consists of a format for storing and transmitting Logiweb pages containing computer programs and formalized mathematics together with a protocol for indexing and locating such pages.
One main software component of the system is the Logiweb compiler (lgc) which can compile computer programs, do automated proof checking, and render programs and proofs in human readable format in the tradition of literate programming. Another main component is the Logiweb abstract machine (lgwam) which can execute programs compiled by lgc.
Logiweb has goals similar to the Mizar system and the QED project. Furthermore, Logiweb has as a goal to offer its users complete notational freedom, to support web publication, and to enable users to use results web-published by other users. Logiweb is free open source available under the GNU license.
History
Design of the system was begun in 1996 by Klaus Grue based on an earlier systems named FL developed 1985-1990 at DIKU. Logiweb was alpha-tested 2004-2006 and beta-tested 2006-2007 at DIKU by graduate students taking courses in Logic. Pre-releases were produced during 2009, and version 1.0.0 is scheduled for release January 2010.
Source language
Logiweb pages are produced by expressing them in Logiweb source (lgs). Lgs is a plain text (Unicode/UTF-8) format. Once a page is expressed in lgs, the lgc compiler is able to compile programs in the source, verify proofs in the source, execute test suites in the source, and render the source in a human readable format.
The syntax of lgs is user definable in that the user defines the syntax he or she wants to use in a header and then uses that syntax in the body of an lgs source text. Furthermore, the rendering produced by lgc is under user control.
The logic against which formal proofs are verified is user definable.
The programming language of Logiweb is lambda calculus with a few, additional operators such a . The programming language is born lazy but the system also supports eager programming. The language is born untyped but allows the user to define a typing disciplin to be checked by the system.

Main Menu

See Also

Main Menu