- Built-in basic types like integers, lists, strings, and so on
- Definite clause grammars
- Static typechecking and polymorphic types/data structures

- Names
`a`,`b`are concrete data inhabiting*name types*. - Names can be bound within terms using an abstraction construction
`n\t`inhabiting abstraction types`tn\tt`. - Names can be swapped with each other, and though there is no built-in notion of substitution of terms for names, capture-avoiding substitution can be defined for object languages.
- 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
`a # t`that can hold between a name and a term

```
``````
id : name_type.
```

exp : type.

var : id -> exp.

app : (exp,exp) -> exp.

lam : id\exp -> exp.

For example, we can encode the identity function as `lam (a\var a)`

.
The standard approach to writing the same code in Prolog or Mercury would require maintaining a source of fresh names (such as an increasing integer tag) throughout the program, and writing more constraints forcing variables to be distinct.
However, in αProlog, capture-avoiding substitution can be written as
follows:
```
``````
func subst(exp,exp,id) = exp.
```

subst(var(x),E,x) = E.

subst(var(y),E,x) = var(y).

subst(app(E1,E2),E,x) = app(subst(E1,E,x),subst(E2,E,x)).

subst(lam(y\E1),E,x) = lam(y\subst(E1,E,x)) :- y # E.

This behaves essentially the same as the explicit version, but the αProlog version is much simpler. There is no need for the programmer to keep track of the details of how names are generated. Instead, name parameters like `x` and `y` stand for arbitrary names (including fresh ones).

Secondly, in the `var` case, instead of testing whether the identifiers with which X and Y are instantiated are the same using if-then-else, we just specify what happens if the two identifiers are the same (the first clause) or different (the second clause). In αProlog, two distinct names are assumed to be semantically distinct, so the first and second clauses don't overlap.

Finally, in αProlog, we can use the built-in binding syntax to express the third clause. Instead of always renaming the bound variable, we just say that the bound name had better not conflict with any free variables in the substituted term `E`. This provides added generality: it might be possible to prove (through program analysis) that a fresh name is not necessary, thus saving the cost of renaming. Also, the execution order of the clauses is no longer fixed by the program, so, an implementation is free to execute them in any order (or in parallel). This was not the case with the traditional version, because there is a data dependency between (for example) the first and second call to `subst`

in the `app`

case.

- Symbolic differentiation
- Regular expressions and automata
- The lambda-mu calculus
- Explicit substitution calculus
- Translation between de Bruijn and nominal formulations of lambda-terms
- A continuation-passing style translation
- An object calculus with translation of lambda-terms (see
*A Theory of Objects*, M. Abadi and L. Cardelli, 1996) - The pi-calculus operational semantics
- Cryptographic authentication protocols (Needham-Schroeder(-Lowe))

αProlog is "alpha" software (no pun intended). The author cannot be held responsible for any problems with this software.

*A simple sequent calculus for nominal logic*, James Cheney. Journal of Logic and Computation, special issue in honor of Roy Dyckhoff. Published online, May 2014.*A dependent nominal type theory*, LMCS volume 8(1:8), 2012 (special issue for TYPES 2010). (arXiv)*Mechanizing the metatheory of LF.*Christian Urban, James Cheney, and Stefan Berghofer. Transactions on Computational Logic. 12(2):A15, January 2011. Formal development here.-
*Nominal Logic Programming*, J. Cheney and C. Urban.*Transactions on Programming Languages and Systems*, 30(5):26 August 2008. *Mechanized Metatheory Model-Checking*, James Cheney and Alberto Momigliano, PPDP 2007 (ACM)*The Semantics of Nominal Logic Programs*, James Cheney. ICLP 2006, p. 361 - 375. (Errata) (Springer)*Towards a General Theory of Names, Binding and Scope*, MERLIN 2005. pp 33-40. (ACM)*Scrap your Nameplate (Functional Pearl)*, James Cheney, ICFP 2005.*Relating Higher-Order Pattern Unification and Nominal Unification*, James Cheney, UNIF 2005*Avoiding Equivariance in Alpha-Prolog*, Christian Urban and James Cheney, TLCA 2005*Equivariant Unification*, James Cheney, RTA 2005*A Simpler Proof Theory for Nominal Logic*, James Cheney, FOSSACS 2005.*Nominal Logic Programming*, James Cheney, PhD dissertation, Cornell University, August 2004. (PDF)*Alpha-Prolog: a logic programming language with names, binding and alpha-equivalence*, James Cheney and Christian Urban. ICLP 2004.*A Sequent Calculus for Nominal Logic*, Murdoch Gabbay and James Cheney. LICS 2004, p. 139-148.*The Complexity of Equivariant Unification*, James Cheney. ICALP 2004.*System Description: alpha-Prolog, a Fresh Approach to Logic Programming Modulo alpha-Equivalence*, James Cheney and Christian Urban. 2003 Workshop on Unification, Valencia, Spain, 2003.

The following papers provide important background material concerning nominal logic, the Gabbay-Pitts formalism, and nominal unification.

- A. M. Pitts,
*Alpha-Structural Recursion and Induction*, Journal of the ACM 53(2006)459-506. - C. Urban, A. M. Pitts and M.J. Gabbay,
*Nominal Unification*, Theoretical Computer Science 323(2004) 473-497. - A. M. Pitts,
*Nominal logic, a first-order theory of names and binding*, Information and Computation 186 (2003) 165-193 - M. J. Gabbay and A. M. Pitts,
*A New Approach to Abstract Syntax with Variable Binding*, Formal Aspects of Computing 13 (2002) 341-363.