|
 ABSTRACT
We propose a sequent calculus derived from the λ―μμ˜-calculus of Curien and Herbelin that is expressive enough to directly represent the fine details of program evaluation using typical abstract machines. Not only does the calculus easily encode the usual components of abstract machines such as environments and stacks, but it can also simulate the transition steps of the abstract machine with just a constant overhead. Technically this is achieved by ensuring that reduction in the calculus always happens at a bounded depth from the root of the term. We illustrate these properties by providing shallow encodings of the Krivine (call-by-name) and the CEK (call-by-value) abstract machines in the calculus.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
M. Abadi , L. Cardelli , P.-L. Curien , J.-J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States
[doi> 10.1145/96709.96712]
|
| |
2
|
|
| |
3
|
|
| |
4
|
|
| |
5
|
|
| |
6
|
|
| |
7
|
Danos, V., Joinet, J.-B., and Schellinx, H. 1993. A new deconstructive logic: Linear logic. In Proceedings of the Workshop on Linear Logic, J.-Y. Girard, et al., Eds.
|
| |
8
|
|
| |
9
|
|
| |
10
|
Felleisen, M., Friedman, D., Kohlbecker, E., and Duba, B. 1986. Reasoning with continuations. In 1st Symposium on Logic and Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 131--141.
|
| |
11
|
Felleisen, M. and Friedman, D. P. 1986. Control operators, the SECD-machine and the λ-calculus. In Formal Description of Programming Language Concepts III. Elsevier, Amsterdam, The Netherlands, 193--217.
|
| |
12
|
|
| |
13
|
Gentzen, G. 1969. Investigations into logical deduction. In Collected Papers of Gerhard Gentzen, M. Szabo, Ed. Elsevier, Amsterdam, The Netherlands, 68--131.
|
| |
14
|
|
| |
15
|
Thérèse Hardin , Luc Maranget , Bruno Pagano, Functional back-ends within the lambda-sigma calculus, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.25-33, May 24-26, 1996, Philadelphia, Pennsylvania, United States
|
| |
16
|
|
| |
17
|
|
| |
18
|
Howard, W. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, J. R. Hindley and J. P. Seldin, Eds. Elsevier, Amsterdam, The Netherlands, 479--490.
|
| |
19
|
Huet, G. and Lévy, J.-J. 1991. Computations in orthogonal rewriting systems, i. In Computational Logic: Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. MIT Press, Cambridge, MA, 395--414.
|
| |
20
|
Jones, M. P. 1998. The functions of Java bytecode. In Proceedings of the OOPSLA Wokshop on the Formal Underpinnings of Java.
|
| |
21
|
Klein, G. and Strecker, M. 2004. Verified bytecode verification and type-certifying compilation. J. Logic Program. 58, 1-2, 27--60. citeseer.ist.psu.edu/article/klein03verified.html.
|
| |
22
|
|
| |
23
|
|
| |
24
|
Liu, H. and Moore, J. S. 2004. Java program verification via a JVM deep embedding in ACL2. In 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004). Lecture Notes in Computer Science, vol. 3223. Springer-Verlag, Berlin, 184--200.
|
| |
25
|
|
| |
26
|
|
| |
27
|
|
| |
28
|
Plotkin, G. D. 1975. Call-by-Name, call-by-value, and the lambda-calculus. Theor. Comput. Sci. 1, 2, 125--159.
|
| |
29
|
Polonovski, E. 2004. Strong normalization of λ―μμ˜-calculus. In Foundations of Software Science and Computation Structures (FOSSACS 2004). Lecture Notes in Computer Science, vol. 2987. Springer-Verlag, Berlin, 423--437.
|
| |
30
|
|
| |
31
|
Prawitz, D. 1965. Natural Deduction, a Proof-Theoretical Study. Almquist and Wiksell, Stockholm.
|
| |
32
|
|
| |
33
|
|
| |
34
|
|
| |
35
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.3