[Prev][Next][Index][Thread]
AlphaProlog 0.3 releae announcement
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
I am pleased to announce the initial public release of AlphaProlog,
version 0.3.
What is AlphaProlog?
--------------------
AlphaProlog is a logic programming language with built-in names, fresh
name generation, name binding, and unification up to alpha-equivalence
(that is, consistent renaming of bound names). Though still in
development, its ultimate aim is to provide a better way of both writing
and reasoning about programs that rely heavily on names and binding,
such as compilers, interpreters, and theorem provers.
AlphaProlog supports a declarative, stateless approach to programming
with names, based on FM, a permutation-based theory of abstract syntax
and binding developed by Gabbay and Pitts and used in the FreshML
programming language, and, more directly, on Pitts's nominal
logic and Urban, Pitts, and Gabbay's nominal unification algorithm.
Languages like Twelf, Qu-Prolog, and Lambda-Prolog also support encoding
names and binding using built-in meta-level variables and bindings.
These languages are semantically much richer and more complex than
AlphaProlog, which is essentially first-order. While these languages
are more mature and provide some features which AlphaProlog lacks, there
are some kinds of programs which are difficult to express using
higher-order encodings but easy to express in AlphaProlog. Examples
include computations involving open terms, fresh name generation, or
varying numbers of bound variables.
This makes AlphaProlog a very useful tool for prototyping languages,
type systems, operational semantics, and logics that sometimes play
the square peg to higher-order encoding techniques' round hole.
Some examples that are included with the AlphaProlog distribution
include:
* The operational semantics of the pi-calculus in its original form
* Regular expression-to-automata translation
* An object calculus and its translation from the lambda-calculus
* A closure-conversion translation
* First-order unification and MiniML type inference
* A natural deduction calculus for Dynamic Logic with proof terms
Features
--------
AlphaProlog has the following features shared by other logic and
functional programming languages:
* Built-in basic types like integers, lists, strings, and terms
* First order Horn clause and definite clause grammar programming
* Static typechecking and polymorphic types and data structures
In addition, AlphaProlog has several new features for programming with
names and binding:
* Names are concrete data inhabiting name types.
* Names can be bound within terms using an abstraction construction
inhabiting abstraction types (distinct from function types).
* Names can be swapped with each other, and though there is no
built-in notion of substitution of terms for names,
capture-avoiding substitution operations are definable.
* Term equality and unification are modulo alpha-equivalence.
* Fresh names are generated automatically as needed during
execution, instead of explicitly (and imperatively) by the
programmer.
* Freshness is an explicit built-in predicate relating names and terms.
Where can I get AlphaProlog?
----------------------------
A source distribution as well as more information about AlphaProlog,
including examples and (draft) documentation, is available at
http://www.cs.cornell.edu/People/jcheney/aprolog/
Questions, comments, and bug reports should be direted to the author at
jcheney@cs.cornell.edu
Related Information
-------------------
More information about FM, nominal logic/unification, and FreshML can
be found at:
http://www.freshml.org/
http://www.cl.cam.ac.uk/~cu200/Unification
--James