Logiweb(TM)

1 Elevator speech

Prev Up Next Page 2 of 800 Search internet


The Logiweb Compiler (lgc) is free software (GNU license) which can

The Logiweb Source (lgs) language is a generic language which allows you to define your own syntax and semantics. As an example, if you want to write about the binomial coefficient "\frac{m!}{n!(m-n)!}" you may decide to

Put your mouse over formulas to see their lgs source text as tooltips.

Logiweb allows you to reference work published by others across the web. As an example, you can write a page which references this definition of Peano Arithmetic PA and then prove e.g. this:

PA lemma 3.2l : all x : 0 * x = 0 end lemma

A proof may look like this.

Cases

Teaching mathematical logic at university level.
Students wrote theses using Logiweb. Formal proofs in theses were verified by Logiweb before the theses were handed in.
Implementation of a star tracker.
A star tracker is a device which, given a camera image of the night sky, recognizes the constellation of stars and computes the direction of sight of the camera. As a test case in the European space industry, star tracker software has been implemented in Logiweb. The conclusion of the study was that doing so can reduce the cost of Independent Software Verification and Validation (ISVV / IV&V).
Implementation of generic proof checker.
The proof checker published here allows you to define your own, formal theory and to verify your proofs against your theory.
Implementation of the Logiweb Compiler (lgc) itself.
Lgc is implemented in its own language.

Properties

The Logiweb programming language is λ-calculus. Programs run efficiently because they are optimized by a factor around "10^9". The language is pure functional and lazy. This makes it easy for you to reason about your programs.

Logiweb also supports eager functional programming. That is built on top of λ-calculus so that one can still reason about the programs.

Despite the pure functional nature, the notion of a Logiweb machine allows to write stand alone programs which interact with their surroundings. The star tracker and the Logiweb compiler mentioned above are examples of such machines.

Logiweb has a good interface to the C programming language.

Future directions

It is the intension to make a version of the Logiweb Abstract Machine which is suited for hard real time applications. This involves a replacement of the current garbage collector and enhancement of interrupt processing. Among other, this will allow to write an operating system using Logiweb.

It is the intension to support imperative programming built on top of λ-calculus just like eager functional programming is already supported. That will allow to run non-Logiweb programs inside the system.

It is the intension to reduce memory requirements. Currently, you need 2 gigabyte RAM to run Logiweb because focus has been on time efficiency only.

It is the intension to implement theories for reasoning about Logiweb programs. Such theories exist, but they need to be expressed in a way that make them compatible with the generic proof checker mentioned above.

What you can do

Download Logiweb, do the tutorial, and use the system. Join the mailing list. Give feedback on the tutorial to grue@diku.dk. Have fun.

Prev Up Next Page 2 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05