Article

A polymorphic modal type system for lisp-like multi-staged languages

Authors:

Cristiano CalcagnoAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 257 - 268

https://doi.org/10.1145/1111037.1111060

Published: 11 January 2006 Publication History

Abstract

This article presents a polymorphic modal type system and its principal type inference algorithm that conservatively extend ML by all of Lisp's staging constructs (the quasi-quotation system). The combination is meaningful because ML is a practical higher-order, impure, and typed language, while Lisp's quasi-quotation system has long evolved complying with the demands from multi-staged programming practices. Our type system supports open code, unrestricted operations on references, intentional variable-capturing substitution as well as capture-avoiding substitution, and lifting values into code, whose combination escaped all the previous systems.

References

[1]

D. Ancona and E. Moggi. A fresh calculus for name management. In Proceedings of the International Conference on Generative Programming and Component Engineering, October 2004.

[2]

Cristiano Calcagno, Eugenio Moggi, and Tim Sheard. Closed types for a safe imperative MetaML. Journal of Functional Programming, 13(3), 2003.

Digital Library

[3]

Cristiano Calcagno, Eugenio Moggi, and Walid Taha. ML-like inference for classifiers. In Proceedings of the European Symposium on Programming 2004, pages 79--93. Springer, 2004.

[4]

Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In Proceedings of the International Conference on Functional Programming (ICFP '02), pages 275--286. ACM, August 2003.

Digital Library

[5]

Olivier Danvy. Type-directed partial evaluation. In Proceedings of the Symposium on Principles of Programming Languages, pages 242--257. ACM, Jan 1996.

Digital Library

[6]

Rowan Davies. A temporal-logic approach to binding-time analysis. In Proceedings of the Symposium on Logic in Computer Science (LICS '96), pages 184--195. IEEE Computer Society Press, 1996.

Digital Library

[7]

Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Proceedings of the Symposium on Principles of Programming Languages (POPL '96), pages 258--270. ACM, 1996.

Digital Library

[8]

Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555--604, 2001.

Digital Library

[9]

Dawson R. Engler. VCODE: A retargetable, extensible, very fast dynamic code generation system. In Proceedings of the Conference on Programming Language Design and Implementation, pages 160--170, New York, 1996. ACM.

Digital Library

[10]

Paul Graham. On Lisp: an advanced techniques for Common Lisp. Prentice Hall, 1994.

Digital Library

[11]

Robert Harper. A simplified account of polymorphic references. Information Processing Letters, 51:201--206, 1994.

Digital Library

[12]

Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation and automatic program generation. Prentice-Hall, 1993.

Digital Library

[13]

Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system for Lisp-like multi-staged languages. Technical Report ROPAS-2005-26, (ropas.snu.ac.kr/lib/dock/KiYiCa2005.pdf), 2005.

[14]

Eugene Kohlbecker, Daniel P. Friedman, Matthias Felleisen, and Bruce Duba. Hygienic macro expansion. In Proceedings of the 1986 ACM Conference on LISP and functional programming, pages 151--161. ACM, August 1986.

Digital Library

[15]

M. Leone and Peter Lee. Optimizing ML with run-time code generation. In Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation, pages 137--148. ACM Press, June 1996.

Digital Library

[16]

H. Massalim. An Efficient Implementation of Functional Operating System Services. PhD thesis, Columbia University, 1992.

Digital Library

[17]

Aleksandar Nanevski. Meta-programming with names and necessity. In Proceedings of the International Conference on Functional Programming (ICFP '02), pages 206--217. ACM, October 2002.

Digital Library

[18]

Aleksandar Nanevski and Frank Pfenning. Staged computation with names and necessity. to appear in Journal of Functional Programming.

Digital Library

[19]

Massimilian Poletto, Wilson C. Hsieh, Dawson R. Engler, and M. Frans Kasshoek. C and tcc:a language and compiler for dynamic code generation. ACM Transactions on Programming Languages and Systems, 21:324--369, March 1999.

Digital Library

[20]

Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1993.

[21]

Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

Digital Library

[22]

Morten Rhiger. First-class open and closed code fragments. In Proceedings of the Sixth Symposium on Trends in Functional Programming, September 2005.

[23]

Guy L. Steele. Common Lisp the Language, 2nd edition. Digital Press, 1990.

Digital Library

[24]

Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, November 1999.

Digital Library

[25]

Walid Taha and Michael Florentin Nielsen. Environment classifiers. In Proceedings of the Symposium on Principles of Programming Languages (POPL '03). ACM, 2003.

Digital Library

[26]

J. B. Wells. The essence of principal typings. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming, pages 913--925. Springer-Verlag, 2002.

Digital Library

[27]

Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343--355, Dec 1995.

Digital Library

Cited By

Murase YNishiwaki YIgarashi A(2023)Contextual Modal Type Theory with Polymorphic ContextsProgramming Languages and Systems10.1007/978-3-031-30044-8_11(281-308)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_11
Jang JGélineau SMonnier SPientka B(2022)Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itselfProceedings of the ACM on Programming Languages10.1145/34987006:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498700
Parreaux LShaikhha AErwig MGray J(2020)Multi-stage programming in the large with staged classesProceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3425898.3426961(35-49)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3425898.3426961
Show More Cited By

Index Terms

A polymorphic modal type system for lisp-like multi-staged languages
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

A polymorphic modal type system for lisp-like multi-staged languages
Proceedings of the 2006 POPL Conference

This article presents a polymorphic modal type system and its principal type inference algorithm that conservatively extend ML by all of Lisp's staging constructs (the quasi-quotation system). The combination is meaningful because ML is a practical ...
Polymorphic type-checking in scheme

This paper presents a type-inference system for Scheme that is designed to be used by students in an introductory programming course. The major goal of the work is to present a type system that is simple enough to be used by beginner students, yet is ...
Extending Dylan's type system for better type inference and error detection
ILC '10: Proceedings of the 2010 international conference on Lisp

Whereas dynamic typing enables rapid prototyping and easy experimentation, static typing provides early error detection and better compile time optimization. Gradual typing [26] provides the best of both worlds. This paper shows how to define and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
Issue’s Table of Contents

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
598
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Murase YNishiwaki YIgarashi A(2023)Contextual Modal Type Theory with Polymorphic ContextsProgramming Languages and Systems10.1007/978-3-031-30044-8_11(281-308)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_11
Jang JGélineau SMonnier SPientka B(2022)Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itselfProceedings of the ACM on Programming Languages10.1145/34987006:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498700
Parreaux LShaikhha AErwig MGray J(2020)Multi-stage programming in the large with staged classesProceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3425898.3426961(35-49)Online publication date: 16-Nov-2020
https://dl.acm.org/doi/10.1145/3425898.3426961
Fromherz AGiannarakis NHawblitzel CParno BRastogi ASwamy N(2019)A verified, efficient embedding of a verifiable assembly languageProceedings of the ACM on Programming Languages10.1145/32903763:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290376
Florence SYou STov JFindler R(2019)A calculus for Esterel: if can, can. if no can, no can.Proceedings of the ACM on Programming Languages10.1145/32903743:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290374
Emmi MEnea C(2019)Weak-consistency specification via visibility relaxationProceedings of the ACM on Programming Languages10.1145/32903733:POPL(1-28)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290373
Meyer RWolff S(2019)Decoupling lock-free data structures from memory reclamation for static analysisProceedings of the ACM on Programming Languages10.1145/32903713:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290371
Skorstengaard LDevriese DBirkedal L(2019)StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilitiesProceedings of the ACM on Programming Languages10.1145/32903323:POPL(1-28)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290332
Miyazaki YSekiyama TIgarashi A(2019)Dynamic type inference for gradual Hindley–Milner typingProceedings of the ACM on Programming Languages10.1145/32903313:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290331
Toro MLabrada ETanter É(2019)Gradual parametricity, revisitedProceedings of the ACM on Programming Languages10.1145/32903303:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290330
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents