There are many interesting and useful ProgrammingLanguageTheoryTextsOnline
has a directory of programmming language websites
Statically typed languages
is a non-strict, polymorphic functional language with type inference and controlled side effects and supports overloading via type classes. Haskell implementations include compilers
and interpreters (GHC and
Most implementations support extensions such as existential types and multiparameter type classes.
is a preprocessor which extends Haskell with the ability to define functions which recurse over types.
is a not-quite-Haskell predecessor of Hugs.
is a Haskell-like language with uniqueness typing.
ML is a strict, polymorphic functional language with uncontrolled side effects, type inference and a powerful system of parametrizable modules.
is a robust compiler with extensions like first-class continuations and higher-order functors. Moscow ML
is a popular lightweight compiler supporting recursive modules.
is a whole-program optimizing compiler.
The ML Kit
is a modular reference implementation of the language.
is a compiler which targets Java.
is a compiler for a variant of Standard ML which targets Microsoft's .NET.
library is part of the standard.
is a Tk interface.
(also see CAML
is a pragmatic ML variant with OO extensions.
has many useful links.
is (nearly) an implementation of CAML which targets .NET.
extends Ocaml with high-level features for distributed programming based on the
is a derivative of Ocaml with compile-time reflection.
Java and C#
Java is a statically typed object-oriented language very similar to C++, which
typically runs atop a virtual machine.
There are a ton of resources and libraries available for Java:
Cafe au Lait Java FAQs, News and Resources
is Microsoft's answer to Java; it runs atop the
which (unlike the Java platform) is intended to support multiple source
is an open source implementation of .NET for UNIX.
is a generic environment for language specification.
is a reflective language based on rewriting logic.
is actually higher-order, but has an algebraic flavor to it.
Other members of this group are:
Joseph Goguen's Hidden Algebra page
Oxford Hidden Algebra page
is a hybrid functional/rule-based language with unification, implied iteration
and deep pattern match.
is a terminating, polymorphic language supporting type inference and
algebraic, and higher-order coalgebraic, datatypes.
is an array programming language based on the idea: Function = Imperative +
is a polymorphic logic/functional language with controlled side effects
supporting static declaration of modes and determinism for logical predicates.
Niklaus Wirth has created several languages of note, all procedural, of which Pascal is
the best known.
(co-designer of C) wrote a famous diatribe,
Why Pascal Is Not My Favorite Programming Language
See also the
Modula-3 Home Page
Digital's SRC Modula-3
Shortcut to the
Modula-3 Language Definition
Oberon is interesting for its tight integration with the Oberon operating
Oberon System V4
The Oberon Reference Site
The Oberon Webring
is a low-level, safe, C-like language with functional features,
generics, modules and resource-tracking types.
is another C-like
language with tagged unions, parametric polymorphism, pattern-matching,
exceptions, structural typing for records and parametrized typedefs.
is an SML variant descended, at least in spirit, from
was originally intended as an extension language for the
computer algebra system AXIOM; it supports dependent and first-class
is a language for specifying program transformations via
is a programming language with dependent types;
type checking in Cayenne is undecidable (i.e., the checker may not terminate),
but the system is extremely expressive.
is a language based on
Milner's pi-calculus, designed to make it easy to define high-level connectors
for composing and coordinating software components written in other
is an OO language based on Java, with parametric types,
higher-order functions and multi-methods.
is a concurrent, object-oriented, functional language with a special focus on
web services, and designed as a successor to
a language based on the Join calculus which combines FP with Petri
is a language from
(of LISP fame) based on speech-acts.
is an OO language that tries to support unplanned reuse of code.
is an OO language that lets dynamically and statically typed code interoperate
via run-time code generation.
Unites Functions and Objects.
is a procedural language with subtyping and parametrizable modules, intended
for heavy-duty military and industrial applications. See also
Ada Core Technologies
home of the GNAT compiler.
is a fast statically typed scripting language.
Logic frameworks, theorem provers and proof assistants
is a proof assistant for pure type systems with subtyping.
is a proof assistant implementing Edinburgh LF, the (Generalized) Calculus of
Constructions and Unified Theory of Dependent Types.
is a generic theorem prover with tactics and tacticals.
is a theorem prover for higher-order logic.
is a theorem prover based on a significant extension of Martin-Lof's
Intuitionistic Type Theory.
is a proof assistant for the Calculus of Inductive Constructions.
is a verification system including a
specification language based on classical, typed, higher-order logic and a
includes the LF framework with type reconstruction, the Elf
constraint logic programming language and an inductive meta-theorem prover for
The Mizar Project
is a long-term effort aimed at developing software to support a working
mathematician in preparing papers, including a natural deduction language for
expressing mathematics over Tarski-Grothendieck set theory.
Dynamically typed languages
Scheme is a minimalist functional language with uncontrolled side effects and
a hygienic macro system. It descends from LISP.
is a full-featured Scheme environment including a graphic IDE, debugger, help
system and GUI library, well-suited for classroom use.
the Scheme Repository
What these languages seem to have in common is that they are all dynamically
typed and procedural, with lots of built-in datatypes and a strong emphasis on
syntax and text-processing. Also, it seems all of them are implemented either
as interpreters, or as compilers targeting a virtual machine, and support
(and the Java-targeting implementation
is an OO language with closures, exceptions and resumptions.
is a single inheritance OO language with closures.
is a desk calculator language with optional static type checking.
is lightweight language designed for extending applications.
is a language with OO extensions and built-in support for text-processing.
supports "goal-directed evaluation".
is a language for gluing applications together and interfacing with the Tk
is based on term rewriting.
is a procedural language developed at IBM. See also
an OO extension, and
which targets Java.
Prolog is the de facto standard here, for intuitionistic logic:
is based on linear logic.
has built-in support for concurrency, distributed computation and fault
tolerance. Erlang is used in several large telecommunication systems at
Objective C is an extension of C with constructs for dynamically typed
object-oriented programming. See
Objective C Resources
is a pure OO language with multi-methods; the Vortex compiler uses a
whole-program optimizer to largely eliminate unnecessary dispatches.
is an updated version of the well known
is a multiparadigm language based on Oz,
which supports declarative programming, object-oriented programming, constraint
programming, and concurrency as part of a coherent whole.
TeX is a typesetting program created by
based on a macro programming language. It is widely used in academia and
research circles, not least because of its unequaled support for mathematical
typography. Many useful macro packages are available from the
is a 16-bit version of TeX supporting Unicode.
is a portal.
converts TeX fonts to Type 1 fonts, which is important for producing PDF files
legible in Acrobat.
is a document formatting system similar to TeX which produces PostScript and PDF.
XML is a markup language related to HTML widely used in industry.
W3C XML Page
the XML Cover Pages
Cafe con Leche XML News and Resources
SGML is a predecessor of XML which is still used in many places. See
SGML Cover Pages
is an ISO standard for formatting and transforming SGML documents,
based on a superset of the Scheme programming language.
is an implementation of DSSSL based on James Clark's earlier
James Clark's DSSSL Page
There is a
DSSSL Mailing List
DESY Literate Programming Library
for a summary.
If it exists (or once did), you will probably find it in the the
Other kinds of information are available at
Programming Language Exploration
Here are some quick links to other programming languages and related projects:
The R Project for Statistical Computing
Styx Scanner & Parser Generator
High Performance Generic Programming Project
the CiME Rewrite Tool
the Internet Virtual Machine
The Great Computer Language Shootout
The Great Win32 Computer Language Shootout
at St. Andrews, and
- 23 Sep 2002