Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
On a Logical Foundation for Explicit Substitutions
| |
|
On a Logical Foundation for Explicit Substitutions
Frank Pfenning1 
| (1) |
Department of Computer Science, Carnegie Mellon University, |
Abstract
Traditionally, calculi of explicit substitution [1] have been conceived as an implementation technique for β-reduction and studied with the tools of rewriting theory. This computational view has been extremely fruitful (see [2] for
a recent survey) and raises the question if there may also be a more abstract underlying logical foundation.
Fulltext Preview (Small, Large)
References
| 1. |
Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416
(1991)
|
| |
| 2. |
Kesner, D.: The theory of calculi with explicit substitutions revisited. Unpublished manuscript (October 2006)
|
| |
| 3. |
Herbelin, H.: A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn,
J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)
|
| |
| 4. |
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. Transactions on Computational Logic (to appear 2007)
|
| |
|
|
|
|
|
|