ConCert Project: Software

The software that is developed as part of the ConCert project can be downloaded from this location.

Mechanized Proofs

C5

Description
Machine-checkable proofs of excluded middle, global soundness and completeness, and type safety for C5.
Requires
Files

Lambda 5

Description
Machine-checkable proofs of cut admissibility, normalization, and (simplified) type safety for Lambda 5.
Requires
Files

ConCert Framework

Conductor v2 Software

Description
This new version of the conductor software forms the infrastructure of the ConCert grid. The software is responsible for distributing and running the certified computations (called "cords") and for interfacing with application software.
Requires
  • TALx86 3.0 with Popcorn
  • MLton to compile the SML source
Versions
  • 2.0 (20 Aug 2003) - Demoable but pre-stable research version.

ConCert v1 Software

Description
The ConCert software implements the scheduling, distribution, and verification of computation on the grid. This software is required to participate on the ConCert grid framework. More documentation about the ConCert software and framework can be found in DeLap's senior thesis [DeL02]. This version is obsoleted by the above.
Requires
  • Objective Caml (OCAML) 3.04 compiler
  • TALx86 3.0 with Popcorn (included)
  • MLton (optional) to build some front-end software.
Versions
  • 0.1 (05/15/2002) - The first pre-release version.

ConCert v1 Simulator

Description
The ConCert Simulator provides a SML library that implements as closely as possible the proposed high-level programming language for programming in ConCert. It does not run tasks on the grid but rather simulates ConCert tasks running on the grid by threads running on the local system. The proposed high-level programming interface cannot be implemented directly in SML, so certain compromises had to be made; however,these were kept to a minimum. More documentation about the proposed high-level programming interface and the simulator can be found in Chang's senior thesis [Cha02].
Requires
  • Standard ML of New Jersey (SML/NJ) 110 compiler with Concurrent ML (CML)
Versions
  • 0.1 (05/15/2002) - The first pre-release version. CML is used to simulate on the local system ConCert tasks running on the grid.

Applications

Iktara - Linear Logic Theorem Prover

Description
Iktara is a linear logic theorem prover intended to run on the ConCert grid framework. The development of Iktara has served to guide the design of a high-level programming interface for programming in ConCert. More documentation about the theorem proving algorithm and the adaptation for the ConCert framework can be found in Chang's senior thesis [Cha02].
Requires
  • Standard ML of New Jersey (SML/NJ) 110 compiler with Concurrent ML (CML)
  • ConCert Simulator
Versions
  • 0.1 (05/15/2002) - The first pre-release version. There are three versions of Iktara: a sequential implementation in SML without any extensions, a concurrent implementation in CML, and an implementation that runs on the ConCert simulator.

Lightharp - Ray Tracer

Description
Lightharp is a parallel ray tracer written in Popcorn to the ICFP 2000 programming contest specification.
Requires
Versions
  • 2.0 (20 Aug 2003) - For Conductor v2.
  • 1.0 (06/14/2002) - First Release.
 

Tempo - Chess Player

Description
Tempo is a parallel chess player written in Popcorn that implements the Jamboree algorithm.
Requires
Versions
  • 2.0 (20 Aug 2003) - For Conductor v2.