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

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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type structure General Terms Languages, Theory Keywords Multi-staged languages, Type systems, Polymo...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Ik-Soon Kim, Kwangkeun Yi, Cristiano Calcagno
• Keywords: General Terms Languages, Intentional Variable-capturing Substitution, POPL 2006, Program Constructs--Type Structure, Programming Languages