Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front Comput Sci Chin    2011, Vol. 5 Issue (3) : 369-380    https://doi.org/10.1007/s11704-011-9106-1
RESEARCH ARTICLE
Static typing for a substructural lambda calculus
Baojian HUA1,2()
1. School of Software Engineering, University of Science and Technology of China, Hefei 230027, China; 2. Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China
 Download: PDF(244 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
Abstract

Substructural type systems are designed from the insight inspired by the development of linear and substructural logics. Substructural type systems promise to control the usage of computational resources statically, thus detect more program errors at an early stage than traditional type systems do. In the past decade, substructural type systems have been deployed in the design of novel programming languages, such as Vault, etc. This paper presents a general typing theory for substructural type system. First, we define a universal semantic framework for substructural types by interpreting them as characteristic intervals composed of type qualifiers. Based on this framework, we present the design of a substructural calculus λSL with subtyping relations. After giving syntax, typing rules and operational semantics for λSL, we prove the type safety theorem. The new calculus λSL can guarantee many more safety invariants than traditional lambda calculus, which is demonstrated by showing that the λSL calculus can serve as an idealized type intermediate language, and defining a type- preserving translation from ordinary typed lambda calculus into λSL.

Keywords Programming languages      linear type systems      substructural type system      subtyping theory      type preserving translation     
Corresponding Author(s): HUA Baojian,Email:bjhua@ustc.edu.cn   
Issue Date: 05 September 2011
 Cite this article:   
Baojian HUA. Static typing for a substructural lambda calculus[J]. Front Comput Sci Chin, 2011, 5(3): 369-380.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-011-9106-1
https://academic.hep.com.cn/fcs/EN/Y2011/V5/I3/369
Fig.1  Partial order between and
Fig.2  Partial order after adding
Fig.3  Types for λ calculus
Fig.4  Definition of function
Fig.5  Typing environment
Fig.6  λ calculus syntax
Fig.7  Typing and subtyping rules for λ
Fig.8  Types in λ calculus
Fig.9  Case study of typing derivations in λ
Fig.10  Operational semantics for λ calculus
Fig.11  calculus syntax
Fig.12  From to λ: types and tying environment
Fig.13  From to λ: terms
1 Girard J Y. Linear logic. Theoretical Computer Science , 1987, 50: 1-102
doi: 10.1016/0304-3975(87)90045-4
2 Girard J Y. On the uinty of logic. Annals of Pure and Applied Logic , 1993, 59(3): 201-217
doi: 10.1016/0168-0072(93)90093-S
3 Wadler P. Linear types can change the world! In: Proceedings of IFIP TC 2 Working Conference on Programming Concepts and Methods . 1990, 347-359
4 Wadler P. Is there a use for linear logic? In: Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation . 1991, 255-273
5 Walker D, Watkins K. On regions and linear types (extended abstract). In: Proceedings of the 6th ACM SIGPLAN international conference on Functional Programming . 2001, 181-192
6 Wansbrough K, Jones S P. Once upon a polymorphic type. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages . 1999, 15-28
7 Kobayashi N. Quasi-linear types. In: Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages . 1999, 29-42
8 Polakow J. Linear logic programming with an ordered context. In: Proceedings of the 2nd ACM SIGPLAN Conference on Principles and Practice of Declarative Programming . 2000, 68-79 .
9 Polakow J, Pfenning F. Ordered linear logic programming. Technical Report CMU-CS-98–183, Department of Computer Science, Carnegie Mellon University , December1998.
10 Smith F, Walker D, Morrisett J G. Alias types. In: Proceedings of 9th European Symposium on Programming . 2000, 366-381
11 Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. In: Proceedings of Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming . 2003, 213-226
12 Walker D. Substructural type systems. In: Pierce B C, eds, Advanced Topics in Types and Programming Languages . Cambridge: MIT Press, 2005
13 Kernighan B W, Ritchie D M. The C programming Language. Upper Saddle River: Prentice-Hall, 1988
14 Foster J S, F?hndrich M, Aiken A. A theory of type qualifiers. In: Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation . 1999, 192-203
15 Foster J S, Terauchi T, Aiken A. Flow-Sensitive Type Qualifiers. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation . 2002, 1-12
16 Polakow J. Ordered linear logic and applications. Dissertation for the Doctoral Degree . Pittsburgh: Carnegie Mellon University, 2001
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed