Semantics of the reFLect language

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Semantics of the reFL^ect language

Full text

Pdf (220 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming table of contents

Verona, Italy

Pages: 32 - 42

Year of Publication: 2004

ISBN:1-58113-819-9

Authors

Sava Krstić	Intel Corporation
John Matthews	OGI School of Science & Engineering at OHSU

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 19, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1013963.1013971 What is a DOI?

ABSTRACT

reFL^ect is a new functional language, developed at Intel for use in hardware design and verification. It contains features intended to facilitate the construction, analysis, and manipulation of the language's own programs. It is also intended to be the executable subset of the term language of a theorem prover based on higher order logic.In this paper, we consider core reFL^ect---a language that extends a polymorphically typed λ-calculus with a datatype for programs and with constructs for splicing programs into programs and for defining functions that inspect and modify programs. We prove that the reduction semantics for this language is strongly normalizing and confluent. We also give a set-theoretical denotational semantics for the language and prove that the reduction semantics is sound with respect to the denotational semantics. These results provide the basis for developing the semantics of reFL^ect's extension of higher order logic and proving its soundness.

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	H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams Iv , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand, Revised Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, v.11 n.1, p.7-105, August 1998 [doi>10.1023/A:1010051815785]
	2	Roberto M. Amadio , Pierre-Louis Curien, Domains and lambda-calculi, Cambridge University Press, New York, NY, 1998
	3	Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
	4	Leo Bachmair , Nachum Dershowitz, Commutation, Transformation, and Termination, Proceedings of the 8th International Conference on Automated Deduction, p.5-20, July 27-August 01, 1986
	5	Gilles Barthe , Horatiu Cirstea , Claude Kirchner , Luigi Liquori, Pure patterns type systems, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-261, January 15-17, 2003, New Orleans, Louisiana, USA
	6	Philippe de Groote, Strong Normalization in a Non-Deterministic Typed Lambda-Calculus, Proceedings of the Third International Symposium on Logical Foundations of Computer Science, p.142-152, July 11-14, 1994
	7	Mariangiola Dezani-Ciancaglini , Ugo de'Liguoro , Adolfo Piperno, A Filter Model for Concurrent $\lambda$-Calculus, SIAM Journal on Computing, v.27 n.5, p.1376-1419, Oct. 1998 [doi>10.1137/S0097539794275860]
	8	J. Grundy, J. O'Leary, and T. Melham. A reflective functional language for hardware design and theorem proving. Technical Report PRG-RR-03-16, Oxford University Computing Laboratory, 2003.
	9	Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
	10	B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.
	11	Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
	12	S. KrstiĆ and J. Matthews. Subject reduction and confluence for the reFLern-2.5pt language. Technical Report CSE-03-014, OGI, 2003.
	13	C.-H. L. Ong. Non-determinism in a functional setting. In 8th Symposium on Logic in Computer Science (LICS), pages 275--286. IEEE Computer Society Press, 1993.
	14	Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
	15	Walid Taha , Tim Sheard, MetaML and multi-stage programming with explicit annotations, Theoretical Computer Science, v.248 n.1-2, p.211-242, October 2000 [doi>10.1016/S0304-3975(00)00053-0]
	16	V. van Oostrom. Lambda calculus with patterns. Technical Report IR-228, Faculteit der Wiskunde en Informatica, Vrije Universiteit Amsterdam, 1990.