- 1.Roberto M. Amadio. Translating Core Facile. Technical Report ECRC-1994-3, ECRC, February 1994.Google Scholar
- 2.Pierre America, Jaco de Bakker, Joost N. Kok. and Jan Rutten. Operational Semantics of a Parallel Object- Oriented Language. in Conf. Rec. 13th A CAd Symposium on Principles of Programming Languages, pages 194-208, 1986. Google ScholarDigital Library
- 3.G. R. Andrews and R. A. Olsson. The SR Programming Language: Concurrency in Practice. Benjamin/Cummings, 1993. Google ScholarDigital Library
- 4.Andrew W. Appel. Compiling w~th Continuations. Cambridge University Press, Cambridge, 1992. Google ScholarDigital Library
- 5.Lennart Augustsson, Mikael Rittri, and Dan Synek. On Generating Unique Names. Journal of Functional Programming, 4:117-123, 1994.Google ScholarCross Ref
- 6.J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge University Press, 1990. Google ScholarDigital Library
- 7.Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1981.Google Scholar
- 8.A. Beguelin, J. Dongarra, A. Geist, R. Manchek, Ko Moore, and V. Sunderamo PVM and HENCE: Tools for Heterogeneous Network Computing. I,n .1. S. Kowalik and L. Grandinetti, editors, Software fol Parallel Computation, volume 106 of NATO AS} Ser~es F. Springer-Verlag, 1993. Google ScholarDigital Library
- 9.Bard Bloom. CHOCOLATE: Calculi of Highm Order COmmunication and LAmbda TErms. In Conf. Rec. 21st A CM Symposium on Principles of Programming Languages, pages 339-347, 1994. Google ScholarDigital Library
- 10.Bard Bloom. Structured Operational Semantics as a Specification Language. In Conf. Rec. 22rid A UM Symposium on Principles of Programming Languages, pages 107-117~ 1995. Google ScholarDigital Library
- 11.Jonathan Bowen, Martin tqanzle, Ernst-Rudiger Olderog, and Anders P. Ravn. Developing Correct Systems. In Proceedings of the 5th Eurom~cro Workshop on Real-Tzme Syst~'m.~ {EEE Computei Society Press, 1993.Google ScholarCross Ref
- 12.William Clinger. l'he Scheme 311 Compiler: An Exercise in Denotational Semantics. In Proc. 1984 A CM Symposium on L~sp and Functional Programming, pages 356-364, August 1984. Google ScholarDigital Library
- 13.Cormac Flanagan and Matthias Felleisen. The Semantics of Future Technical Report COMP TR94-238~ Rice University, Department of Computer Science Oc{obeI 1994Google Scholar
- 14.G. A. Geist and V. S. Sunderam. The PVM System: Supercomputer Level Concurrent Computation on a Heterogeneous Network of Workstations. In Swcth Annua~ Distributed-Memory Computer Conference, pages 258- 261, 1991.Google ScholarCross Ref
- 15.Alessandro Giacalone, Prateek Mlshra, and Sanjiva Prasad. Facile: A Symmetric Integration of Concurrent and Functional Programming. Internatzonal Journal of Parallel Programming, 18{2):121-160, 1989. Google ScholarDigital Library
- 16.Alessandro Giacalone, Prateek Mishra, and Sanjiva Prasad. Operational and Algebraic Semantics for Facile: A Symmetric Integration of Concurrent attd Functional Programming. In Proc. ICALP '90, volume 443 of Lecture Notes ~n Computer Science, pages 765-7780, Berlin, Heidelberg, and New York, 1990. Springer-Verlag. Google Scholar
- 17.David Gladstein. Compiler Correctness for Concurrent Languages. PhD thesis, Northeastern University, December 1994. Google ScholarDigital Library
- 18.Andrew D. Gordon. Functzonal Programming and Input/Output. Cambridge University Press, Cambridge, 1994. Google ScholarDigital Library
- 19.Michael J. C. Gordon. The Denotat, onalDescrgptzon of Programmgng Languages. Springer-Verlag, Berlin, Heidelberg, New York, 1979. Google ScholarDigital Library
- 20.Michael J. C. Gordon and T. F. Melham. introduction to HOL: A Theorem Proving Enwronment for Higher- Order Logic. Cambridge Universitv Press, Cambridge. 1993. Google ScholarDigital Library
- 21.J. D. Guttman, V. Swarup, and J~ Ramsdell. The VLISP Verified Scheme System. Lisp and Symbolic Computation, 8(1/2), 1995. to appear. Google ScholarDigital Library
- 22.Matthew Hennessy and Robin Milner. AlgebrMc Laws for Nondeterminism and Concurrency. Journal of the ACM. 32:137-161, 1985. Google ScholarDigital Library
- 23.Robin Milner. Operational and Algebraic Semantics of Concurrent Processes. in Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 1201-1242. MIT Press/Elsevier, 1990. Google ScholarDigital Library
- 24.Robin Milner. Functions as Processes. Mathematical Structures ~n Computer Science, 2:119-141, 1992.Google Scholar
- 25.Robin Milner, .Joachim Parrow, and D. Walker A calculus of mobile processes (parts I and II). Information a~d Computatzon. 100:1-77, 1992. Google ScholarDigital Library
- 26.Torben A~. Mogensen. Efficient Self-Interpretation in Lambda CMculus~ Journal of Funct~o~al Proctramm~r~g, pages 345-364, June 1992.Google Scholar
- 27.J. Strother Moore A Mechanicadlv Verified I. anp, uage Implementation. Journal of Auto~ftated /~er/_solltr~y, 5(4):461-492, December 1989. Google ScholarDigital Library
- 28.Flemming Nielson and Hanne Riis Nlel~on. F~om C ML to Process Algebras. In Proceesings o/CONCUR '93, pages 493-508, Berlin, Heidelberg, and New York, 1993. Springer-Verlag. Google Scholar
- 29.Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP Verified PreScheme Compiler. L~sp and Symbolic Computatzon, 8(1/2), 1995. to appear. Google ScholarDigital Library
- 30.David A. Schmidt. Denotational Semantics: A Methodology/or Language Development. Allyn and Bacon. Boston~ 1986~ Google ScholarDigital Library
- 31.Bent Thomsen. A Calculus of Higher Order Communicating Systems. In Conf. Rec. 16th A UM Symposium on Prznciples of Programming Languages, pages 143-154, 1989. Google ScholarDigital Library
- 32.Christopher P. Wadsworth. Some Unusual X-calculus Numeral Systems. In J. P. Hindley and J. R. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Galculus and Formalism, pages 215-230. Academic Press, New York and London, 1980.Google Scholar
- 33.David Walker. ,r-Calculus Semantics of Object- Oriented Programming Languages. In Ptoc. court ret~ce on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Berlin, Heidelberg, and New York, 1991. Springer-Verlag. Google ScholarDigital Library
- 34.Mitchell Wand. Deriving Target Code as a Representation of Continuation Semantics. A CM Transactzons on Programming Languages and Systems, 4(3):496-517, July 1982. Google ScholarDigital Library
- 35.Mitchell Wand. Semantics-Directed Machine Architecture. in Conf. Rec. 9th A CM Symposium on Pr~nczples of Programming Languages, pages 234-241, 1982. Google ScholarDigital Library
- 36.Mitchell Wand. Loops in Combinator-Based Compilers. Information and Control, 57(2-3):148-164, May/June 1983. Google ScholarDigital Library
- 37.Mitchell Wand. A Short Proof of the Lexical Addressing Algorithm. Information Processtng Letters, 35:1-5, 1990. Google ScholarDigital Library
- 38.Mitchell Wand and Dino P. Oliva. Proving the Correctness of Storage Representations. In Proc. 199~ A CM Symposium on Lisp and Functional Programming, pages 151-160, 1992. Google ScholarDigital Library
- 39.Cui Zhang, Brian R. Becket, Mark R. Heckman, Karl Legitt, and Ron A. Olsson. A Hiera.rchical Method for Reasoning about Distributed Programming Languages and its Applications. submitted for pubhcation, t995.Google Scholar
- 40.Cui Zhang, Rob Shaw, Mark R. Heckman, Gregory D. Benson, Myla Archer, Karl Levitt, and Ronald A. Olsson. Towards a Formal Verification of a Secure Distributed System and its Applications. In Proceedings o/ the 17th National Computer Security Conference, pages 103-113, Baltimore, October 1994.Google Scholar
Index Terms
- Compiler correctness for parallel languages
Comments