Skip to content

Latest commit

 

History

History
781 lines (776 loc) · 59.7 KB

ProgrammingLanguages.md

File metadata and controls

781 lines (776 loc) · 59.7 KB

ProgrammingLanguages

There are many interesting and useful ProgrammingLanguageTheoryTextsOnline.

Google has a directory of programmming language websites.

Statically typed languages

Haskell

Haskell is a non-strict, polymorphic functional language with type inference and controlled side effects and supports overloading via type classes. Haskell implementations include compilers (GHC, NHC98, HBC) and interpreters (GHC and Hugs). Most implementations support extensions such as existential types and multiparameter type classes. Generic Haskell is a preprocessor which extends Haskell with the ability to define functions which recurse over types.

Gofer is a not-quite-Haskell predecessor of Hugs. Concurrent Clean is a Haskell-like language with uniqueness typing.

ML

ML is a strict, polymorphic functional language with uncontrolled side effects, type inference and a powerful system of parametrizable modules. SML FAQ, ML FAQ, Info. SML/NJ is a robust compiler with extensions like first-class continuations and higher-order functors. Moscow ML is a popular lightweight compiler supporting recursive modules. MLton is a whole-program optimizing compiler. The ML Kit is a modular reference implementation of the language. MLj is a compiler which targets Java. SML.NET is a compiler for a variant of Standard ML which targets Microsoft's .NET. The new SML Basis library is part of the standard. SML/Tk is a Tk interface.

Objective Caml (also see CAML) is a pragmatic ML variant with OO extensions. ocaml.org has many useful links. F# is (nearly) an implementation of CAML which targets .NET. JoCaml extends Ocaml with high-level features for distributed programming based on the join calculus. MetaOCaml 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. Tutorial, Latest JDK, JavaBeans, Gamelan, Pizza, GJ. There are a ton of resources and libraries available for Java: BluePrints, Developer Connection, jars.com, Java Foundry at SourceForge, jGuru, Cafe au Lait Java FAQs, News and Resources.

C# is Microsoft's answer to Java; it runs atop the .NET platform, which (unlike the Java platform) is intended to support multiple source languages. C# Corner, C# Today, C# Help. Mono is an open source implementation of .NET for UNIX.

Algebraic languages

ASF+SDF is a generic environment for language specification. Maude is a reflective language based on rewriting logic. OPAL is actually higher-order, but has an algebraic flavor to it. Other members of this group are: OBJ and CafeOBJ. Also see Joseph Goguen's Hidden Algebra page and the Oxford Hidden Algebra page. TXL is a hybrid functional/rule-based language with unification, implied iteration and deep pattern match.

Charity is a terminating, polymorphic language supporting type inference and algebraic, and higher-order coalgebraic, datatypes. FISh is an array programming language based on the idea: Function = Imperative + Shape.

Logic languages

Mercury is a polymorphic logic/functional language with controlled side effects supporting static declaration of modes and determinism for logical predicates.

Wirth's languages

Niklaus Wirth has created several languages of note, all procedural, of which Pascal is the best known. Pascal Central. Brian Kernighan (co-designer of C) wrote a famous diatribe, Why Pascal Is Not My Favorite Programming Language. See also the Modula-3 Home Page and Digital's SRC Modula-3. Shortcut to the Modula-3 Language Definition. Oberon is interesting for its tight integration with the Oberon operating system. See: ETH Oberon, Oberon Microsystems, Oberon System V4, The Oberon Reference Site and The Oberon Webring.

Experimental

Vault is a low-level, safe, C-like language with functional features, generics, modules and resource-tracking types. Cyclone is another C-like language with tagged unions, parametric polymorphism, pattern-matching, exceptions, structural typing for records and parametrized typedefs. Alice is an SML variant descended, at least in spirit, from Mozart. Aldor was originally intended as an extension language for the computer algebra system AXIOM; it supports dependent and first-class types. Stratego is a language for specifying program transformations via rewriting strategies. Cayenne 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.

Piccola 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 languages. Nice is an OO language based on Java, with parametric types, higher-order functions and multi-methods. Scala is a concurrent, object-oriented, functional language with a special focus on web services, and designed as a successor to Funnel, a language based on the Join calculus which combines FP with Petri nets.

Elephant 2000 is a language from John McCarthy (of LISP fame) based on speech-acts. TOM is an OO language that tries to support unplanned reuse of code. Transframe is an OO language that lets dynamically and statically typed code interoperate via run-time code generation. UFO Unites Functions and Objects.

Procedural

Ada 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.

Pike is a fast statically typed scripting language.

Logic frameworks, theorem provers and proof assistants

Yarrow is a proof assistant for pure type systems with subtyping. LEGO is a proof assistant implementing Edinburgh LF, the (Generalized) Calculus of Constructions and Unified Theory of Dependent Types. Isabelle is a generic theorem prover with tactics and tacticals. HOL is a theorem prover for higher-order logic. Nuprl is a theorem prover based on a significant extension of Martin-Lof's Intuitionistic Type Theory.

COQ is a proof assistant for the Calculus of Inductive Constructions. PVS is a verification system including a specification language based on classical, typed, higher-order logic and a theorem prover. Twelf includes the LF framework with type reconstruction, the Elf constraint logic programming language and an inductive meta-theorem prover for LF.

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

Scheme is a minimalist functional language with uncontrolled side effects and a hygienic macro system. It descends from LISP. DrScheme is a full-featured Scheme environment including a graphic IDE, debugger, help system and GUI library, well-suited for classroom use. Gambit Scheme, Bigloo, (Petite) Chez Scheme, QScheme, SXM, SISC, Schemers.Org, the Scheme Repository.

Scripting languages

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 garbage collection.

Python (and the Java-targeting implementation Jython) is an OO language with closures, exceptions and resumptions. Ruby is a single inheritance OO language with closures. Nickle is a desk calculator language with optional static type checking. Lua is lightweight language designed for extending applications. Perl is a language with OO extensions and built-in support for text-processing. Icon supports "goal-directed evaluation". Tcl is a language for gluing applications together and interfacing with the Tk graphical toolkit. The Q language is based on term rewriting. Rexx is a procedural language developed at IBM. See also Object Rexx, an OO extension, and NetRexx, which targets Java.

Logic languages

Prolog is the de facto standard here, for intuitionistic logic: SWI-Prolog, SICStus Prolog, GNU Prolog, YAP Prolog, XSB.

Lygon is based on linear logic.

Other

Erlang has built-in support for concurrency, distributed computation and fault tolerance. Erlang is used in several large telecommunication systems at Ericsson. See also Gerl.

Objective C is an extension of C with constructs for dynamically typed object-oriented programming. See Objective C Resources at swarm.org.

Cecil is a pure OO language with multi-methods; the Vortex compiler uses a whole-program optimizer to largely eliminate unnecessary dispatches.

StarLogo is an updated version of the well known LOGO language.

Mozart is a multiparadigm language based on Oz, which supports declarative programming, object-oriented programming, constraint programming, and concurrency as part of a coherent whole.

Document languages

Typesetting

TeX is a typesetting program created by Donald Knuth, 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 CTAN servers. Omega is a 16-bit version of TeX supporting Unicode. (La)TeX Navigator is a portal. TeXtrace converts TeX fonts to Type 1 fonts, which is important for producing PDF files legible in Acrobat.

Lout is a document formatting system similar to TeX which produces PostScript and PDF.

Markup languages

XML is a markup language related to HTML widely used in industry. See the W3C XML Page, the XML Cover Pages, xml.com and Cafe con Leche XML News and Resources.

SGML is a predecessor of XML which is still used in many places. See SGML Cover Pages. DSSSL is an ISO standard for formatting and transforming SGML documents, based on a superset of the Scheme programming language. OpenJade is an implementation of DSSSL based on James Clark's earlier Jade (also James Clark's DSSSL Page). There is a DSSSL Mailing List.

Literate Programming

See the DESY Literate Programming Library for a summary.

Miscellaneous

If it exists (or once did), you will probably find it in the the Language List. Other kinds of information are available at Inter-Language Unification and Programming Language Exploration.

Here are some quick links to other programming languages and related projects: the SUIF Compiler, Sisal, Lolli, Poplog, Sather, The R Project for Statistical Computing, merd, Flare, Styx Scanner & Parser Generator, High Performance Generic Programming Project, the CiME Rewrite Tool, avram, the Internet Virtual Machine, The Great Computer Language Shootout, The Great Win32 Computer Language Shootout, Leda.

Broken links: Napier88 at St. Andrews, and KiR at Kiel.

-- FrankAtanassow - 23 Sep 2002

ProgrammingLanguageTheoryTextsOnline

This is a collection of programming language theory texts and resources, all of which are freely available over the Internet.

Many valuable reference texts on programming language theory, previously only available in paper form, have in recent years become publicly accessible from the net. I list here the ones I know of; below that you will also find a much broader list of lecture notes and tutorials, other interesting reading, plus a collection of related resources.

Obligatory plea

If you know of any other texts or resources which might belong here, please add them to this list by editing this page. (Does your submission belong in this list? See the #SubmissionGuidelines.)

I hope other authors will also make an effort, when possible, to get their books online, especially if the book goes out of print.

Part of the reason PL theory and advanced programming languages seem impenetrable to other communities is that learning materials are hard to obtain, or demand a sizeable investment of resources (time, money, ...) even if the potential reader is only exploring the subject.

Reference texts

Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. (MIT)

Hassan Ait-Kaci. Warren's Abstract Machine: A Tutorial Reconstruction. (link)

Andrea Asperti and Giussepe Longo. Categories, Types and Structures. An introduction to Category Theory for the working computer scientist. (link)

Henk Barendregt. Lambda Calculi with Types. (compressed PS)

--. The Lambda Calculus. (currently broken link)

Michael Barr and Charles Wells. Toposes, Triples and Theories. (link)

Stanley N. Burris and H.P. Sankappanavar. A Course in Universal Algebra. (link)

Hubert Comon, et al. Tree Automata Techniques and Applications. (link)

Reinhard Diestel. Graph Theory. (link)

Raphael Finkel. Advanced Programming Language Design. (link)

Dick Grune and Ceriel J.H. Jacobs. Parsing Techniques - A Practical Guide. (link)

Robert Harper. Programming Languages: Theory and Practice. (Draft) (link)

Matthew Hennessy. Semantics of Programming Languages. (gzipped PS/2up, Andrew Pitts' course material)

N.D. Jones, C.K. Gomard and P. Sestoft. Partial Evaluation and Automatic Program Generation. (link)

Carroll Morgan. Programming from Specifications. (link)

Susumu Hayashi and Hiroshi Nakano. PX: A Computational Logic. (PDF, link)

Hanne Riis Nielson and Flemming Nielson. Semantics With Applications: A Formal Introduction. (link)

Bengt Nordstrom and Kent Petersson and Jan M. Smith. Programming in Martin-Lof's Type Theory: An Introduction. (link)

Simon Peyton Jones and David R. Lester. Implementing functional languages: a tutorial. (link, compressed PS, sources)

Rinus Plasmeijer and Marko van Eekelen. Functional Programming and Parallel Graph Rewriting. (link)

Scott F. Smith. Programming Languages. (link)

Paul Taylor. Practical Foundations of Mathematics. (link)

Simon Thompson. Type Theory and Functional Programming. (link)

Notes and tutorials

Luca Cardelli and Peter Wegner. On understanding types, data abstraction and polymorphism. (PS/letter, PDF/letter, PS/A4, PDF/A4)

Giuseppe Castagna. Subtyping and Object-oriented Programming. (course page, gzipped PS)

Robert Constable. Typed Logic. (link, HTML, PS)

Jean H. Gallier. Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi. (compressed DVI)

--. Constructive Logics. Part II: Linear Logic and Proof Nets. (link, compressed DVI, compressed PS)

--. On the Correspondence between Proofs and lambda-Terms. (compressed PS)

Mike Gordon. Introduction to Functional Programming. (link)

--. Specification and Verification I. (link - 2000 ed.)

--. Specification and Verification II. (link - 1999 ed.)

John Harrison. Introduction to Functional Programming (1996/7). (link)

Achim Jung and Samson Abramsky. Domain Theory. (gzipped PS)

Alexander Kurz. Coalgebras and Modal Logic. (link)

Per Martin-Lof. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. (link)

Bengt Nordstrom, Kent Petersson and Jan M. Smith. Martin-Lof's Type Theory. (gzipped PS)

Lawrence C. Paulson. Foundations of Functional Programming. (link)

Frank Pfenning. Automated Theorem Proving. (link)

--. Computation and Deduction. (link)

Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. (gzipped PS)

Andrew M. Pitts. Lecture Notes on Types. (link)

--. Operational Semantics and Program Equivalence. (PS)

--. Categorical Logic. (gzipped PS)

Gordon Plotkin. Pisa Notes (on Domain Theory). (link, gzipped PS, gzipped PS/A4)

Giuseppe Rosolini. Sheaves. (gzipped PS: A4, US)

Helmut Schwichtenberg. Proof Theory. (compressed PS, compressed DVI)

Morten Heine B. Sorenson and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. (gzipped PS)

Thomas Streicher. Fibred Categories. (gzipped PS)

Other texts

Texts in this section are interesting, though not directly related to programming language theory.

G.J. Chaitin. The Unknowable. (link)

Philip J. Koopman, Jr. Stack Computers: the new wave. (link)

Resources

If you are interested in these topics, you can find additional resources (mostly in the forms of technical articles and theses) via:

Submission guidelines

Most importantly, any submission must include a URL to the full text of the manuscript: this is not an online list of texts, but rather a list of online texts. Also, the text should be freely accessible; so, texts which belong to some sort of private digital library (like the ACM Digital Library or Elsevier's collection) are not admissible.

This list focuses on book-length reference works which treat major topics in programming language theory, mathematical semantics and foundations, particularly texts which have gone out of print. It would be nice if we could assemble a set of texts which are representative of a master's degree curriculum in programming language theory or computational mathematics.

On the other hand, do not dismiss interesting-looking material only because it is too short, or because it does not treat a central topic, or because it is too specific. If you know of something valuable which does not quite fit the guidelines above, consider putting it in the #OtherTexts category.

Dissertations, theses and technical articles are not really suitable for this list, unless they provide an accessible (or: the unique) introduction to, or tutorial for, a relatively broad and/or important topic. Conversely, a survey would need to treat its topic in considerable depth to be included here.

Lecture notes and tutorials are acceptable, provided they are readable as self-contained manuscripts. Because there are so many manuscripts here of this type, please try to submit material which minimizes overlap with existing entries.

Administration

This Wiki page is adapted from my (FrankAtanassow's) PLT Online page.

For now, both versions will coexist and I will probably add any updates to this page to my own page as well, and vice versa. If this Wiki version sees a lot of activity and takes off, and does not evolve too far from my original purpose (outlined in the #SubmissionGuidelines above), then I may trash my page and redirect page views to this Wiki.

-- FrankAtanassow - 23 Sep 2002