Common Lisp

History

Work on Common Lisp started in 1981 after an initiative by ARPA manager Bob Engelmore to develop a single community standard Lisp dialect. Much of the initial language design was done via electronic mail. In 1982, Guy L. Steele Jr. gave the first overview of Common Lisp at the 1982 ACM Symposium on LISP and functional programming.

The first language documentation was published in 1984 as Common Lisp the Language (known as CLtL1), first edition. A second edition (known as CLtL2), published in 1990, incorporated many changes to the language, made during the ANSI Common Lisp standardization process: extended LOOP syntax, the Common Lisp Object System, the Condition System for error handling, an interface to the pretty printer and much more. But CLtL2 does not describe the final ANSI Common Lisp standard and thus is not a documentation of ANSI Common Lisp. The final ANSI Common Lisp standard then was published in 1994. Since then no update to the standard has been published. Various extensions and improvements to Common Lisp (examples are Unicode, Concurrency, CLOS-based IO) have been provided by implementations and libraries.

Syntax

Common Lisp is a dialect of Lisp. It uses S-expressions to denote both code and data structure. Function calls, macro forms and special forms are written as lists, with the name of the operator first, as in these examples:

Data types

Common Lisp has many data types.

Scalar types

Number types include integers, ratios, floating-point numbers, and complex numbers. Common Lisp uses bignums to represent numerical values of arbitrary size and precision. The ratio type represents fractions exactly, a facility not available in many languages. Common Lisp automatically coerces numeric values among these types as appropriate.

The Common Lisp character type is not limited to ASCII characters. Most modern implementations allow Unicode characters.

The symbol type is common to Lisp languages, but largely unknown outside them. A symbol is a unique, named data object with several parts: name, value, function, property list, and package. Of these, value cell and function cell are the most important. Symbols in Lisp are often used similarly to identifiers in other languages: to hold the value of a variable; however there are many other uses. Normally, when a symbol is evaluated, its value is returned. Some symbols evaluate to themselves, for example, all symbols in the keyword package are self-evaluating. Boolean values in Common Lisp are represented by the self-evaluating symbols T and NIL. Common Lisp has namespaces for symbols, called 'packages'.

A number of functions are available for rounding scalar numeric values in various ways. The function round rounds the argument to the nearest integer, with halfway cases rounded to the even integer. The functions truncate, floor, and ceiling round towards zero, down, or up respectively. All these functions return the discarded fractional part as a secondary value. For example, (floor -2.5) yields −3, 0.5; (ceiling -2.5) yields −2, −0.5; (round 2.5) yields 2, 0.5; and (round 3.5) yields 4, −0.5.

Data structures

Sequence types in Common Lisp include lists, vectors, bit-vectors, and strings. There are many operations that can work on any sequence type.

As in almost all other Lisp dialects, lists in Common Lisp are composed of conses, sometimes called cons cells or pairs. A cons is a data structure with two slots, called its car and cdr. A list is a linked chain of conses or the empty list. Each cons's car refers to a member of the list (possibly another list). Each cons's cdr refers to the next cons—except for the last cons in a list, whose cdr refers to the nil value. Conses can also easily be used to implement trees and other complex data structures; though it is usually advised to use structure or class instances instead. It is also possible to create circular data structures with conses.

Common Lisp supports multidimensional arrays, and can dynamically resize adjustable arrays if required. Multidimensional arrays can be used for matrix mathematics. A vector is a one-dimensional array. Arrays can carry any type as members (even mixed types in the same array) or can be specialized to contain a specific type of members, as in a vector of bits. Usually, only a few types are supported. Many implementations can optimize array functions when the array used is type-specialized. Two type-specialized array types are standard: a string is a vector of characters, while a bit-vector is a vector of bits.

Hash tables store associations between data objects. Any object may be used as key or value. Hash tables are automatically resized as needed.

Packages are collections of symbols, used chiefly to separate the parts of a program into namespaces. A package may export some symbols, marking them as part of a public interface. Packages can use other packages.

Structures, similar in use to C structs and Pascal records, represent arbitrary complex data structures with any number and type of fields (called slots). Structures allow single-inheritance.

Classes are similar to structures, but offer more dynamic features and multiple-inheritance. (See CLOS). Classes have been added late to Common Lisp and there is some conceptual overlap with structures. Objects created of classes are called Instances. A special case is Generic Functions. Generic Functions are both functions and instances.

Functions

Common Lisp supports first-class functions. For instance, it is possible to write functions that take other functions as arguments or return functions as well. This makes it possible to describe very general operations.

The Common Lisp library relies heavily on such higher-order functions. For example, the sort function takes a relational operator as an argument and key function as an optional keyword argument. This can be used not only to sort any type of data, but also to sort data structures according to a key.

The evaluation model for functions is very simple. When the evaluator encounters a form (f a1 a2...) then it presumes that the symbol named f is one of the following:

A special operator (easily checked against a fixed list)

A macro operator (must have been defined previously)

The name of a function (default), which may either be a symbol, or a sub-form beginning with the symbol lambda.

If f is the name of a function, then the arguments a1, a2, ..., an are evaluated in left-to-right order, and the function is found and invoked with those values supplied as parameters.

The macro defun defines functions where a function definition gives the name of the function, the names of any arguments, and a function body:

Function definitions may include compiler directives, known as declarations, which provide hints to the compiler about optimization settings or the data types of arguments. They may also include documentation strings (docstrings), which the Lisp system may use to provide interactive documentation:

Anonymous functions (function literals) are defined using lambda expressions, e.g. (lambda (x) (* x x)) for a function that squares its argument. Lisp programming style frequently uses higher-order functions for which it is useful to provide anonymous functions as arguments.

Other types

Other data types in Common Lisp include:

Pathnames represent files and directories in the file system. The Common Lisp pathname facility is more general than most operating systems' file naming conventions, making Lisp programs' access to files broadly portable across diverse systems.

Input and output streams represent sources and sinks of binary or textual data, such as the terminal or open files.

Common Lisp has a built-in pseudorandom number generator (PRNG). Random state objects represent reusable sources of pseudo-random numbers, allowing the user to seed the PRNG or cause it to replay a sequence.

Conditions are a type used to represent errors, exceptions, and other "interesting" events to which a program may respond.

Classes are first-class citizens, and are themselves instances of classes called metaobject classes or metaclasses.

Readtables are a type of object which control how Common Lisp's reader parses the text of source code. By controlling which readtable is in use when code is read in, the programmer can change or extend the language's syntax.

Scope

Like programs in many other programming languages, Common Lisp programs make use of names to refer to variables, functions, and many other kinds of entities. Named references are subject to scope.

The association between a name and the entity which the name refers to is called a binding.

Scope refers to the set of circumstances in which a name is determined to have a particular binding.

Determiners of scope

The circumstances which determine scope in Common Lisp include:

the location of a reference within an expression. If it's the leftmost position of a compound, it refers to a special operator or a macro or function binding, otherwise to a variable binding or something else.

the kind of expression in which the reference takes place. For instance, (go x) means transfer control to label x, whereas (print x) refers to the variable x. Both scopes of x can be active in the same region of program text, since tagbody labels are in a separate namespace from variable names. A special form or macro form has complete control over the meanings of all symbols in its syntax. For instance, in (defclass x (a b) ()), a class definition, the (a b) is a list of base classes, so these names are looked up in the space of class names, and x isn't a reference to an existing binding, but the name of a new class being derived from a and b. These facts emerge purely from the semantics of defclass. The only generic fact about this expression is that defclass refers to a macro binding; everything else is up to defclass.

the location of the reference within the program text. For instance, if a reference to variable x is enclosed in a binding construct such as a let which defines a binding for x, then the reference is in the scope created by that binding.

for a variable reference, whether or not a variable symbol has been, locally or globally, declared special. This determines whether the reference is resolved within a lexical environment, or within a dynamic environment.

the specific instance of the environment in which the reference is resolved. An environment is a run-time dictionary which maps symbols to bindings. Each kind of reference uses its own kind of environment. References to lexical variables are resolved in a lexical environment, et cetera. More than one environment can be associated with the same reference. For instance, thanks to recursion or the use of multiple threads, multiple activations of the same function can exist at the same time. These activations share the same program text, but each has its own lexical environment instance.

Kinds of environment

Some environments in Lisp are globally pervasive. For instance, if a new type is defined, it is known everywhere thereafter. References to that type look it up in this global environment.

One type of environment in Common Lisp is the dynamic environment. Bindings established in this environment have dynamic extent, which means that a binding is established at the start of the execution of some construct, such as a let block, and disappears when that construct finishes executing: its lifetime is tied to the dynamic activation and deactivation of a block. However, a dynamic binding is not just visible within that block; it is also visible to all functions invoked from that block. This type of visibility is known as indefinite scope. Bindings which exhibit dynamic extent (lifetime tied to the activation and deactivation of a block) and indefinite scope (visible to all functions which are called from that block) are said to have dynamic scope.

Common Lisp has support for dynamically scoped variables, which are also called special variables. Certain other kinds of bindings are necessarily dynamically scoped also, such as restarts and catch tags. Function bindings cannot be dynamically scoped using flet (which only provides lexically scoped function bindings), but function objects (a first-level object in Common Lisp) can be assigned to dynamically scoped variables, bound using let in dynamic scope, then called using funcall or APPLY.

Dynamic scope is extremely useful because it adds referential clarity and discipline to global variables. Global variables are frowned upon in computer science as potential sources of error, because they can give rise to ad-hoc, covert channels of communication among modules that lead to unwanted, surprising interactions.

In Common Lisp, a special variable which has only a top-level binding behaves just like a global variable in other programming languages. A new value can be stored into it, and that value simply replaces what is in the top-level binding. Careless replacement of the value of a global variable is at the heart of bugs caused by the use of global variables. However, another way to work with a special variable is to give it a new, local binding within an expression. This is sometimes referred to as "rebinding" the variable. Binding a dynamically scoped variable temporarily creates a new memory location for that variable, and associates the name with that location. While that binding is in effect, all references to that variable refer to the new binding; the previous binding is hidden. When execution of the binding expression terminates, the temporary memory location is gone, and the old binding is revealed, with the original value intact. Of course, multiple dynamic bindings for the same variable can be nested.

Macros

A macro in Lisp superficially resembles a function in usage. However, rather than representing an expression which is evaluated, it represents a transformation of the program source code. The macro gets the source it surrounds as arguments, binds them to its parameters and computes a new source form. This new form can also use a macro. The macro expansion is repeated until the new source form does not use a macro. The final computed form is the source code executed at runtime.

Typical uses of macros in Lisp:

new control structures (example: looping constructs, branching constructs)

scoping and binding constructs

simplified syntax for complex and repeated source code

top-level defining forms with compile-time side-effects

data-driven programming

embedded domain specific languages (examples: SQL, HTML, Prolog)

implicit finalization forms

Various standard Common Lisp features also need to be implemented as macros, such as:

the standard setf abstraction, to allow custom compile-time expansions of assignment/access operators

with-accessors, with-slots, with-open-file and other similar WITH macros

Depending on implementation, if or cond is a macro built on the other, the special operator; when and unless consist of macros

The powerful loop domain-specific language

Example using a macro to define a new control structure

Macros allow Lisp programmers to create new syntactic forms in the language. One typical use is to create new control structures. The example macro provides an until looping construct. The syntax is:

The macro definition for until:

tagbody is a primitive Common Lisp special operator which provides the ability to name tags and use the go form to jump to those tags. The backquote ` provides a notation that provides code templates, where the value of forms preceded with a comma are filled in. Forms preceded with comma and at-sign are spliced in. The tagbody form tests the end condition. If the condition is true, it jumps to the end tag. Otherwise, the provided body code is executed and then it jumps to the start tag.

An example of using the above until macro:

The code can be expanded using the function macroexpand-1. The expansion for the above example looks like this:

During macro expansion the value of the variable test is (= (random 10) 0) and the value of the variable body is ((write-line "Hello")). The body is a list of forms.

Symbols are usually automatically upcased. The expansion uses the TAGBODY with two labels. The symbols for these labels are computed by GENSYM and are not interned in any package. Two go forms use these tags to jump to. Since tagbody is a primitive operator in Common Lisp (and not a macro), it will not be expanded into something else. The expanded form uses the when macro, which also will be expanded. Fully expanding a source form is called code walking.

In the fully expanded (walked) form, the when form is replaced by the primitive if:

All macros must be expanded before the source code containing them can be evaluated or compiled normally. Macros can be considered functions that accept and return S-expressions – similar to abstract syntax trees, but not limited to those. These functions are invoked before the evaluator or compiler to produce the final source code. Macros are written in normal Common Lisp, and may use any Common Lisp (or third-party) operator available.

Variable capture and shadowing

Common Lisp macros are capable of what is commonly called variable capture, where symbols in the macro-expansion body coincide with those in the calling context, allowing the programmer to create macros wherein various symbols have special meaning. The term variable capture is somewhat misleading, because all namespaces are vulnerable to unwanted capture, including the operator and function namespace, the tagbody label namespace, catch tag, condition handler and restart namespaces.

Variable capture can introduce software defects. This happens in one of the following two ways:

In the first way, a macro expansion can inadvertently make a symbolic reference which the macro writer assumed will resolve in a global namespace, but the code where the macro is expanded happens to provide a local, shadowing definition which steals that reference. Let this be referred to as type 1 capture.

The second way, type 2 capture, is just the opposite: some of the arguments of the macro are pieces of code supplied by the macro caller, and those pieces of code are written such that they make references to surrounding bindings. However, the macro inserts these pieces of code into an expansion which defines its own bindings that accidentally captures some of these references.

The Scheme dialect of Lisp provides a macro-writing system which provides the referential transparency that eliminates both types of capture problem. This type of macro system is sometimes called hygienic, in particular by its proponents (who regard macro systems which do not automatically solve this problem as unhygienic).

In Common Lisp, macro hygiene is ensured one of two different ways.

One approach is to use gensyms: guaranteed-unique symbols which can be used in a macro-expansion without threat of capture. The use of gensyms in a macro definition is a manual chore, but macros can be written which simplify the instantiation and use of gensyms. Gensyms solve type 2 capture easily, but they are not applicable to type 1 capture in the same way, because the macro expansion cannot rename the interfering symbols in the surrounding code which capture its references. Gensyms could be used to provide stable aliases for the global symbols which the macro expansion needs. The macro expansion would use these secret aliases rather than the well-known names, so redefinition of the well-known names would have no ill effect on the macro.

Condition system

The condition system is responsible for exception handling in Common Lisp. It provides conditions, handlers and restarts. Conditions are objects describing an exceptional situation (for example an error). If a condition is signaled, the Common Lisp system searches for a handler for this condition type and calls the handler. The handler can now search for restarts and use one of these restarts to automatically repair the current problem, using information such as the condition type and any relevant information provided as part of the condition object, and call the appropriate restart function.

These restarts, if unhandled by code, can be presented to users (as part of a user interface, that of a debugger for example), so that the user can select and invoke one of the available restarts. Since the condition handler is called in the context of the error (without unwinding the stack), full error recovery is possible in many cases, where other exception handling systems would have already terminated the current routine. The debugger itself can also be customized or replaced using the *debugger-hook* dynamic variable. Code found within unwind-protect forms such as finalizers will also be executed as appropriate despite the exception.

In the following example (using Symbolics Genera) the user tries to open a file in a Lisp function test called from the Read-Eval-Print-LOOP (REPL), when the file does not exist. The Lisp system presents four restarts. The user selects the Retry OPEN using a different pathname restart and enters a different pathname (lispm-init.lisp instead of lispm-int.lisp). The user code does not contain any error handling code. The whole error handling and restart code is provided by the Lisp system, which can handle and repair the error without terminating the user code.

Common Lisp Object System (CLOS)

Common Lisp includes a toolkit for object-oriented programming, the Common Lisp Object System or CLOS. Peter Norvig explains how many Design Patterns are simpler to implement in a dynamic language with the features of CLOS (Multiple Inheritance, Mixins, Multimethods, Metaclasses, Method combinations, etc.).

Several extensions to Common Lisp for object-oriented programming have been proposed to be included into the ANSI Common Lisp standard, but eventually CLOS was adopted as the standard object-system for Common Lisp. CLOS is a dynamic object system with multiple dispatch and multiple inheritance, and differs radically from the OOP facilities found in static languages such as C++ or Java. As a dynamic object system, CLOS allows changes at runtime to generic functions and classes. Methods can be added and removed, classes can be added and redefined, objects can be updated for class changes and the class of objects can be changed.

CLOS has been integrated into ANSI Common Lisp. Generic functions can be used like normal functions and are a first-class data type. Every CLOS class is integrated into the Common Lisp type system. Many Common Lisp types have a corresponding class. There is more potential use of CLOS for Common Lisp. The specification does not say whether conditions are implemented with CLOS. Pathnames and streams could be implemented with CLOS. These further usage possibilities of CLOS for ANSI Common Lisp are not part of the standard. Actual Common Lisp implementations use CLOS for pathnames, streams, input–output, conditions, the implementation of CLOS itself and more.

Compiler and interpreter

A Lisp interpreter directly executes Lisp source code provided as Lisp objects (lists, symbols, numbers, ...) read from s-expressions. A Lisp compiler generates bytecode or machine code from Lisp source code. Common Lisp allows both individual Lisp functions to be compiled in memory and the compilation of whole files to externally stored compiled code (fasl files).

Several implementations of earlier Lisp dialects provided both an interpreter and a compiler. Unfortunately often the semantics were different. These earlier Lisps implemented lexical scoping in the compiler and dynamic scoping in the interpreter. Common Lisp requires that both the interpreter and compiler use lexical scoping by default. The Common Lisp standard describes both the semantics of the interpreter and a compiler. The compiler can be called using the function compile for individual functions and using the function compile-file for files. Common Lisp allows type declarations and provides ways to influence the compiler code generation policy. For the latter various optimization qualities can be given values between 0 (not important) and 3 (most important): speed, space, safety, debug and compilation-speed.

There is also a function to evaluate Lisp code: eval. eval takes code as pre-parsed s-expressions and not, like in some other languages, as text strings. This way code can be constructed with the usual Lisp functions for constructing lists and symbols and then this code can be evaluated with the function eval. Several Common Lisp implementations (like Clozure CL and SBCL) are implementing eval using their compiler. This way code is compiled, even though it is evaluated using the function eval.

The file compiler is invoked using the function compile-file. The generated file with compiled code is called a fasl (from fast load) file. These fasl files and also source code files can be loaded with the function load into a running Common Lisp system. Depending on the implementation, the file compiler generates bytecode (for example for the Java virtual machine), C language code (which then is compiled with a C compiler) or, directly, native code.

Common Lisp implementations can be used interactively, even though the code gets fully compiled. The idea of an Interpreted language thus does not apply for interactive Common Lisp.

Code examples

Birthday paradox

The following program calculates the smallest number of people in a room for whom the probability of unique birthdays is less than 50% (the birthday paradox, where for 1 person the probability is obviously 100%, for 2 it is 364/365, etc.). The answer is 23.

In Common Lisp, by convention, constants are enclosed with + characters.

Calling the example function using the read–eval–print loop (REPL):

Sorting a list of person objects

First, define a class person and a method for displaying the name and age of a person. Then, define a group of persons as a list of person objects. Then, iterate over the sorted list.

It prints the three names with descending age.

Exponentiating by squaring

Use of the LOOP macro is demonstrated:

Example use:

Compare with the built in exponentiation:

Find the list of available shells

WITH-OPEN-FILE is a macro that opens a file and provides a stream. When the form is returning, the file is automatically closed. FUNCALL calls a function object. The LOOP collects all lines that match the predicate.

The function AVAILABLE-SHELLS calls the above function LIST-MATCHING-LINES with a pathname and an anonymous function as the predicate. The predicate returns the pathname of a shell or NIL (if the string is not the filename of a shell).

Example results (on Mac OS X 10.6):

Comparison with other Lisps

Common Lisp is most frequently compared with, and contrasted to, Scheme—if only because they are the two most popular Lisp dialects. Scheme predates CL, and comes not only from the same Lisp tradition but from some of the same engineers—Guy Steele, with whom Gerald Jay Sussman designed Scheme, chaired the standards committee for Common Lisp.

Common Lisp is a general-purpose programming language, in contrast to Lisp variants such as Emacs Lisp and AutoLISP which are extension languages embedded in particular products (GNU Emacs and AutoCAD, respectively). Unlike many earlier Lisps, Common Lisp (like Scheme) uses lexical variable scope by default for both interpreted and compiled code.

Most of the Lisp systems whose designs contributed to Common Lisp—such as ZetaLisp and Franz Lisp—used dynamically scoped variables in their interpreters and lexically scoped variables in their compilers. Scheme introduced the sole use of lexically scoped variables to Lisp; an inspiration from ALGOL 68. CL supports dynamically scoped variables as well, but they must be explicitly declared as "special". There are no differences in scoping between ANSI CL interpreters and compilers.

Common Lisp is sometimes termed a Lisp-2 and Scheme a Lisp-1, referring to CL's use of separate namespaces for functions and variables. (In fact, CL has many namespaces, such as those for go tags, block names, and loop keywords). There is a long-standing controversy between CL and Scheme advocates over the tradeoffs involved in multiple namespaces. In Scheme, it is (broadly) necessary to avoid giving variables names that clash with functions; Scheme functions frequently have arguments named lis, lst, or lyst so as not to conflict with the system function list. However, in CL it is necessary to explicitly refer to the function namespace when passing a function as an argument—which is also a common occurrence, as in the sort example above.

CL also differs from Scheme in its handling of Boolean values. Scheme uses the special values #t and #f to represent truth and falsity. CL follows the older Lisp convention of using the symbols T and NIL, with NIL standing also for the empty list. In CL, any non-NIL value is treated as true by conditionals, such as if, whereas in Scheme all non-#f values are treated as true. These conventions allow some operators in both languages to serve both as predicates (answering a Boolean-valued question) and as returning a useful value for further computation, but in Scheme the value '() which is equivalent to NIL in Common Lisp evaluates to true in a Boolean expression.

Implementations

See the Category Common Lisp implementations.

Common Lisp is defined by a specification (like Ada and C) rather than by one implementation (like Perl). There are many implementations, and the standard details areas in which they may validly differ.

In addition, implementations tend to come with extensions, which provide functionality not covered in the standard:

Interactive Top-Level (REPL)

Garbage Collection

Debugger, Stepper and Inspector

Weak data structures (hash tables)

Extensible sequences

Extensible LOOP

Environment access

CLOS Meta-object Protocol

CLOS based extensible streams

CLOS based Condition System

Network streams

Persistent CLOS

Unicode support

Foreign-Language Interface (often to C)

Operating System interface

Java Interface

Threads and Multiprocessing

Application delivery (applications, dynamic libraries)

List of implementations

Allegro Common Lisp

For Microsoft Windows, FreeBSD, Linux, Apple macOS and various Unix variants. Allegro CL provides an integrated development environment (IDE) (for Windows and Linux) and extensive capabilities for application delivery.

Liquid Common Lisp

Formerly named Lucid Common Lisp. Only maintenance, no new releases.

LispWorks

for Microsoft Windows, FreeBSD, Linux, Apple macOS, iOS, Android, and various Unix variants. LispWorks provides an integrated development environment (IDE) (available for most platforms, but not for iOS and Android) and extensive abilities for application delivery.

mocl

For iOS, Android, and macOS.

Open Genera

For DEC Alpha.

Scieneer Common Lisp

Designed for high-performance scientific computing.

Armed Bear Common Lisp (ABCL)

A CL implementation that runs on the Java virtual machine. It includes a compiler to JVM bytecode, and allows access to Java libraries from CL. It was formerly one component of the Armed Bear J Editor.

Clasp

An LLVM-based implementation that seamlessly interoperates with C++ libraries. Runs on several Unix and Unix-like systems, including macOS.

CLISP

A bytecode-compiling implementation, portable and runs on several Unix and Unix-like systems, including macOS, on Microsoft Windows and several other systems.

Applications

Common Lisp is used to develop research applications (often in Artificial Intelligence), for rapid development of prototypes or for deployed applications.

Common Lisp is used in many commercial applications, including the Yahoo! Store web-commerce site, which originally involved Paul Graham and was later rewritten in C++ and Perl. Other notable examples include:

ACT-R, a cognitive architecture used in a large number of research projects.

Authorizer's Assistant, a large rule-based system used by American Express, analyzing credit requests.

Cyc, a long running project to create a knowledge-based system that provides a huge amount of common sense knowledge.

Gensym G2, a real-time expert system and business rules engine

Genworks GDL, based on the open-source Gendl kernel.

The development environment for the Jak and Daxter video game series, developed by Naughty Dog.

ITA Software's low fare search engine, used by travel websites such as Orbitz and Kayak.com and airlines such as American Airlines, Continental Airlines and US Airways.

Mirai, a 3D graphics suite, known for having been used to design the character of Gollum in The Lords of the Rings movies.

Opusmodus is a music composition system based on Common Lisp, used in Computer assisted composition.

Prototype Verification System (PVS), a mechanized environment for formal specification and verification.