(Submitted to a special issue of JFP on dependently typed programming)

Another motivation was the observation that locally-named representation and locally nameless representation are both too permissive in defining raw terms. Some terms could not have meaning because they contain free occurrences of some local variables which are subject to be bound. It is a distinctive feature of (McKinna & Pollack 1999) that they introduced a way of avoiding appeal to such well-formedness considerations except in a very small number of places such as the definition of typing rules.

In order to remove the necessity of using extra syntax for well-formed terms at all, we use

Finally, we were interested in the utility of simultaneous substitution. Although some people have already showed the importance of simultaneous substitution in formal reasoning about languages with binding, we believed that there were still some hidden properties about it. For example, there are cases where simultaneous substitution is not a choice, but a must. Moreover, simultaneous substitution can be used in saving infrastructure for a formal reasoning.

*When locally-named becomes nominal.*Gyesik Lee, Hugo Herbelin and SunYoung Kim.

Submitted to JFP special issue on dependently typed programming.*Technical report.*Gyesik Lee, Hugo Herbelin, and SunYoung Kim.

A supplementary report on technical issues.

- Trace-Based Locally-Named Representation
- LJT and Kripke Semantics Without Parameters:

- LJT and Kripke Semantics With Parameters:

- LJT and Kripke Semantics Without Parameters:
- Coquand-McKinna-Pollak Style Locally-Named Representation
- LJT and Kripke Semantics Without Parameters:
- LJT and Kripke Semantics With Parameters:

- Locally Nameless Representation
- Soundness of Simply-typed Lambda Calculus:

Trace-based Locally-Named Representation |
LJT and Kripke Semantics Without Parameters | Source |
---|---|---|

LJT and Kripke Semantics With Parameters | Source | |

Coquand-McKinna-Pollack's Locally-named Representation |
LJT and Kripke Semantics Without Parameters | Source |

LJT and Kripke Semantics With Parameters | Source | |

Locally Nameless Representation |
Soundness of Simply-typed Lambda Calculus | Source |

- Coquand, Catarina. A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic Computation 15(1):57-90, 2002.
- Herbelin, Hugo and Lee, Gyesik. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Logic, Language, Information and Computation, 16th International Workshop, Wollic 2009, LNAI 5514:209-217, 2009.
- Leroy, Xavier. A locally nameless solution to the POPLmark challenge. Tecnical report, 6908 (INRIA), 2007.
- McBride, Conor and McKinna, James. The view from the left. Journal of functional programming, 14(1):69-111, 2004.
- McKinna, James and Pollack, Randy. Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3-4):373-409, 1999.
- Stoughton, Allen. Substitution Revisited. Theoretical computer science, 59:317-325, 1988.