David Sands
- Abr90.S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison Wesley, 1990. Google Scholar
Digital Library
- Ale92.F. Alexandre. A technique for transforming logic programs by fold-unfold transformations. In PLILP '92, volume 631 of LNCS, pages 202-216. Springer-Verlag, 1992. Google Scholar
- Amt92.T. Amtoft. Unfold/fold transformations preserving termination properties. In PLILP '92, volume 631 of LNCS, pages 187-201. Springer-Verlag, 1992. Google Scholar
- Amt93.T. Amtoft. Sharing of computations. PhD thesis, DAIMI, Aahus University, 1993.Google Scholar
- BCE92.A. Bossi, N. Cocco, and S. Etalle. Transforming normal programs by replacement. In Third Workshop on Meta-Programming in Logic, META 92, 1992. Google ScholarDigital Library
- BD77.R. Burstall and J. Darlington. A transformation system for developing recursive programs. JA CM, 24:44-67, January 1977. Google ScholarDigital Library
- Deb88.S. Debray. Unfold/fold transformations and loop optimization of logic programs, in Proceedings of the SIGPLAN'88 Conference on Programming Language Design and Implementation, pages 297-307, 1988. SIGPLAN Notices 23(7). Google ScholarDigital Library
- FFK87.M. Felleisen, D. Friedman, and E. Kohlbecker. A syntactic theory of sequential control. Theoretical Computer Science, 52:205-237, 1987. Google ScholarDigital Library
- FN88.Y. Futamura and K. Nogi. Generalised partial computation, in D. BjCrner, Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation. Proceedings of the IFIP TC2 Workshop, Caramel Averna~s, Denmark, October 198Z North-Holland, 1988.Google Scholar
- GK93.R. Gliick and A. V. Klimov. Occam's razor in metacomputation: the notion of a perfect process tree. In G.Filb P.Cousot, M.Falaschi and A.Rauzy, editors, Static Analysis. Proceedings, volume 724 of LNCS, pages 112-123. Springer-Verlag, 1993. Google ScholarDigital Library
- How89.D. J. Howe. Equality in lazy computation systems. In Fourth annual symposium on Logic In Computer Science, pages 198-203. IEEE, 1989. Google Scholar
- Kot78.L. Kott. About transformation system: A theoretical study. In B. Robinet, editor, Program Transformations, pages 232-247. Dunod, 1978.Google Scholar
- Mas86.I. Mason. The Semantics of Destructive Lisp. Number 5 in CSLI Lecture Notes. CSLI, 1986. Google ScholarDigital Library
- Mil77.R. Milner. Fully abstract models of the typed )~-calculus. Theoretical Computer Science, 4, 1977.Google Scholar
- MW79.Z. Manna and R. Waldinger. Synthesis: Dreams -+ programs. Transactions on Programming Languages and Systems, 5(4), 1979.Google Scholar
- Plo75.G.D. Plotkin. Call-by-name, Call-by-value and the X-calculus. Theoretical Computer Science, 1(1):125-159, 1975.Google ScholarCross Ref
- RFJ89.C. Runciman, M. Firth, and N. Jagger. Transformation in a non-strict language: An approach to instantiation. In Functional Programming, Glasgow 1989: Proceedings of the First Glasgow Workshop on Functional Programming, Workshops in Computing. Springer Verlag, August 1989. Google ScholarDigital Library
- San91.D. Sands. Operational theories of improvement in functional languages (extended abstract), in Proceedings of the Fourth Glasgow Workshop on Functional Programming, pages 298-311, Skye, August 1991. Springer Workshop Series. Google ScholarDigital Library
- San94.D. Sands. Total ~)rrectness and improvement in the transformation of functional programs. DIKU, Univelrsity of Copenhagen, Unpublished (53 pages), May 1994.Google Scholar
- San95a.D. Sands. Correctness of recursion-based automatic program transformations. In International Joint Conference on Theory and Practice of Software Development (TAP- 80FT/FASE '95), LNCS. Springer-Verlag, 1995. Google ScholarDigital Library
- San95b.D. Sands. Total correctness by local improvement in program transformation, in Proceedings of the ~2nd Annual A GM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press, January 1995. Google ScholarDigital Library
- Sch80.W. Scherlis. Expression Procedures and Program Derivation. PhD thesis, Dept. of Computer Science, Stanford, 1980. Report No. STAN-CS-80-818. Google ScholarDigital Library
- Sch81.W.L. Scherlis. Pro/~,~arn improvement by internal specialisation. In 8'th Symposium on Principals of Programming Languages. ACM, 1981. Google ScholarDigital Library
- SGJ94.M. H. Sorensen, R. Gliick, and N. D. Jones. Towards unifying partial evaluation, deforestation, supercompilation, and GPC. In ESOP'94. LNCS 788, Springer Verlag, 1994. Google ScholarDigital Library
- Sør94.M H Sorensen. Turchin's supercompiler revisited: An operational theory of positive information propagation. Master's thesis, Department of Computer Science, University of Copenhagen, 1994.Google Scholar
- TS84.H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In S. Tarnlund, editor, ~nd International Logic Programming Conference, pages 1'~7-138, 1984.Google Scholar
- Tur86.V.F. Turchin. The: concept of a supercompiler. ToPLaS, 8:292-325, July 1986. Google ScholarDigital Library
- Wad90.P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73:231-248, 1990. Preliminary version in ESOP 88, LNCS 300. Google ScholarDigital Library
- Weg76.B. Wegbreit. Goal-directed program transformation. IEEE Tran,~actions on Sofware Engineering, 2:69-80, June 1976.Google Scholar
Index Terms
- Higher-order expression procedures
Recommendations
HOL-λσ: an intentional first-order expression of higher-order logic
We give a first-order presentation of higher-order logic based on explicit substitutions. This presentation is intentionally equivalent to the usual presentation of higher-order logic based on λ-calculus, that is, a proposition can be proved without the ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and PracticeHigher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...
Comments