Locally Installed Packages
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 highlevel, stronglytyped, functional and objectoriented programming language from the ML family of languages. Version 3.06.

Hugs  Hugs 98 is an interpreter for the lazy functional programming language Haskell 98.

Moscow ML  Moscow ML provides a lightweight implementation of full Standard ML, including modules and some extensions.

Poly/ML  Poly/ML is a full implementation of Standard ML available as opensource. This version is a beta release supporting the SML97 version of the language and the Standard Basis Library.

SMLNJ  Standard ML of New Jersey. SML/NJ is an interactive compiler for the Standard ML Programming Language (1997 Revision).

EML  Extended ML (EML) is a framework for specification and formal development of Standard ML (SML) programs.

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.

Isabelle  Isabelle is a generic theorem prover.

Jape  Jape  A Framework for building Interactive Proof Editors

LEGO  LEGO is an interactive proof development system (proof assistant).

ProofGeneral  Proof General is a generic Emacs interface for proof assistants.

HOLCASL  HOLCASL is a theorem proving system for CASL. It is based on the generic theorem prover Isabelle.

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.
