[an error occurred while processing this directive] An error occured whilst processing this directive

Software installed locally

Programming Languages · Theorem Provers

This page lists the software packages requested by people in LFCS and installed on Linux machines within the inf.ed.ac.uk domain.

Note that some of the packages listed here are also used for teaching and are the responsibility of support. They are listed here because they may be relevant to research interests in LFCS.

A separate page describes software distributed by LFCS to the wider world.

Programming Languages

Several programming languages, most functional, used for both teaching and research.

Name Brief details
Ocaml Objective Caml is a high-level, strongly-typed, functional and object-oriented programming language from the ML family of languages. Version 3.06.
  • Commands: ocamlc (bytecode compiler), ocamlopt (optimizing native code compiler), ocaml (interactive toplevel system), ocamllex and ocamlyacc (lexer and parser generators)
  • Local Documentation: Reference manual (HTML and Postscript) in /usr/share/doc/ocaml-3.06/
Hugs Hugs 98 is an interpreter for the lazy functional programming language Haskell 98.
Moscow ML Moscow ML provides a light-weight implementation of full Standard ML, including modules and some extensions.
  • Commands: mosml(interpreter), mosmlc (compiler), mosmllex, mosmlyac (lexer and parser generators)
  • Local Documentation: Available in /usr/share/doc/mosml-2.00
This package is maintained by Informatics Support
Poly/MLPoly/ML is a full implementation of Standard ML available as open-source. This version is a beta release supporting the SML97 version of the language and the Standard Basis Library.
  • Commands: poly (interactive SML)
SML-NJ Standard ML of New Jersey. SML/NJ is an interactive compiler for the Standard ML Programming Language (1997 Revision).
  • Commands: sml (interactive SML), sml-cm (SML compilation manager), ml-burg, ml-lex (lexer generator), ml-yacc (parser generator)
EMLExtended ML (EML) is a framework for specification and formal development of Standard ML (SML) programs.
  • Commands: emosml
  • Local Documentation: Don Sannella's EML web page.

Theorem Provers

There is a long history of research on automated reasoning, theorem proving, and type theory in LFCS.

Name Brief details
Coq Coq is a proof assistant based on the Calculus of Inductive Constructions.
  • Commands: coqtop (interactive top-level system), coqc (compiler), can also use ProofGeneral (see below)
IsabelleIsabelle is a generic theorem prover.
  • Commands: Isabelle (start up XEmacs with ProofGeneral interface for Isabelle), isabelle (startup PolyML interpreter with some pre-loaded heap-image), isatool (start various Isabelle tools)
  • Local Documentation: /usr/share/Isabelle2002/doc/
Jape Jape - A Framework for building Interactive Proof Editors This package is maintained by Informatics Support
LEGOLEGO is an interactive proof development system (proof assistant).
  • Commands: lego, legoML
ProofGeneral Proof General is a generic Emacs interface for proof assistants.
HOL-CASL HOL-CASL is a theorem proving system for CASL. It is based on the generic theorem prover Isabelle.
  • Commands: HOL-CASL (interactive top-level)
  • Local Documentation: Some demos and documentation in /usr/lib/HOL-CASL/
cryptyc The Cryptyc system is a Cryptographic Protocol Type Checker. Unlike most typecheckers, it does not just check for simple data errors, such as dereferencing an integer or treating a pointer as a boolean. It can also statically check for security violations such as secrecy or authenticity errors.
An error occured whilst processing this directive