research-article

Intersection types for a λ-calculus with global store

Authors:

Ugo de'Liguoro,

Riccardo TregliaAuthors Info & Claims

PPDP '21: Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming

Article No.: 5, Pages 1 - 11

https://doi.org/10.1145/3479394.3479400

Published: 07 October 2021 Publication History

Abstract

We study the semantics of an untyped λ-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side effects and treat read and write as algebraic operations over a monad. We introduce an operational semantics and a type assignment system of intersection types, and prove that types are invariant under reduction and expansion of term and state configurations, and characterize convergent terms via their typings.

References

[1]

S. Abramsky. 1991. Domain Theory in Logical Form. Ann. Pure Appl. Log. 51, 1-2 (1991), 1–77. https://doi.org/10.1016/0168-0072(91)90065-T

[2]

S. Abramsky and C.-H.L. Ong. 1993. Full abstraction in the lazy lambda calculus. Inf. Comput. 105, 2 (1993), 159–267. https://doi.org/10.1006/inco.1993.1044

Digital Library

[3]

H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completeness of Type Assignment. J. Symb. Log. 48, 4 (1983), 931–940. https://doi.org/10.2307/2273659

[4]

H. P. Barendregt, W. Dekkers, and R. Statman. 2013. Lambda Calculus with Types. Cambridge University Press.

[5]

N. Benton, J. Hughes, and E. Moggi. 2002. Monads and Effects. In Applied Semantics, International Summer School, APPSEM 2000(Lecture Notes in Computer Science, Vol. 2395). Springer, 42–122. https://doi.org/10.1007/3-540-45699-6_2

[6]

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, António Porto and Francisco Javier López-Fraguas (Eds.). ACM, 301–312. https://doi.org/10.1145/1599410.1599447

Digital Library

[7]

N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. 2006. Reading, Writing and Relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006, Proceedings(Lecture Notes in Computer Science, Vol. 4279). Springer, 114–130. https://doi.org/10.1007/11924661_7

Digital Library

[8]

U. Dal Lago, F. Gavazzo, and P. B. Levy. 2017. Effectful Applicative Bisimilarity: Monads, Relators, and Howe’s Method. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Computer Society, 1–12. https://doi.org/10.1109/LICS.2017.8005117

[9]

R. Davies and F. Pfenning. 2000. Intersection types and computational effects. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM, 198–208. https://doi.org/10.1145/351240.351259

Digital Library

[10]

D. de Carvalho. 2018. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci. 28, 7 (2018), 1169–1203. https://doi.org/10.1017/S0960129516000396

[11]

U. de’Liguoro and R. Treglia. 2020. The untyped computational λ-calculus and its intersection type discipline. Theor. Comput. Sci. 846(2020), 141–159. https://doi.org/10.1016/j.tcs.2020.09.029

[12]

U. de’Liguoro and R. Treglia. 2021. From semantics to types: the case of the imperative λ-calculus. (2021). To appear in Proceedings of MFPS 2021.

[13]

U. de’Liguoro and R. Treglia. 2021. Intersection Types for a Computational Lambda-Calculus with Global State. arxiv:2104.01358 [cs.LO]

[14]

M. Dezani-Ciancaglini and S. Ronchi Della Rocca. 2007. Intersection and Reference Types. In Reflections on Type Theory, Lambda Calculus, and the Mind. Radboud University Nijmegen, 77–86. http://www.di.unito.it/~dezani/papers/dr.pdf

[15]

C. Faggian, G. Guerrieri, U. de’Liguoro, and R. Treglia. 2021. On reduction and normalization in the computational core. CoRR abs/2104.10267(2021). arxiv:2104.10267https://arxiv.org/abs/2104.10267

[16]

M. Felleisen and D. P. Friedman. 1989. A Syntactic Theory of Sequential State. Theor. Comput. Sci. 69, 3 (1989), 243–287. https://doi.org/10.1016/0304-3975(89)90069-8

Digital Library

[17]

F. Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph.D. Dissertation. University of Bologna, Italy. http://amsdottorato.unibo.it/9075/

[18]

D. K. Gifford and J. M. Lucassen. 1986. Integrating Functional and Imperative Programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986, August 4-6, 1986, Cambridge, Massachusetts, USA. ACM, 28–38.

Digital Library

[19]

J.-L Krivine. 1993. Lambda calculus, types and models. Ellis Horwood.

[20]

U. Dal Lago and F. Gavazzo. 2019. Effectful Normal Form Bisimulation. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings(Lecture Notes in Computer Science, Vol. 11423), Luís Caires (Ed.). Springer, 263–292. https://doi.org/10.1007/978-3-030-17184-1_10

[21]

U. Dal Lago, F. Gavazzo, and R. Tanaka. 2020. Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci. 813(2020), 234–247. https://doi.org/10.1016/j.tcs.2019.12.025

Digital Library

[22]

J.C. Mitchell. 1996. Foundations for Programming Languages. MIT Press, Cambridge, MA.

Digital Library

[23]

E. Moggi. 1988. Computational Lambda-calculus and Monads. Report ECS-LFCS-88-66. University of Edinburgh, Edinburgh, Scotland.

[24]

E. Moggi. 1991. Notions of Computation and Monads. Inf. Comput. 93, 1 (1991), 55–92. https://doi.org/10.1016/0890-5401(91)90052-4

Digital Library

[25]

A. Pitts and I. Stark. 1998. Operational Reasoning for Functions With Local State. In In Higher Order Operational Techinques in Semantics. Cambridge University Press, 227–273.

[26]

G. D. Plotkin and J. Power. 2002. Notions of Computation Determine Monads. In FOSSACS 2002(Lecture Notes in Computer Science, Vol. 2303). Springer, 342–356. https://doi.org/10.1007/3-540-45931-6_24

[27]

G. D. Plotkin and J. Power. 2003. Algebraic Operations and Generic Effects. Appl. Categorical Struct. 11, 1 (2003), 69–94. https://doi.org/10.1023/A:1023064908962

[28]

J. Power. 2006. Generic models for computational effects. Theor. Comput. Sci. 364, 2 (2006), 254–269.

Digital Library

[29]

J.C. Reynolds. 2000. An Intrinsic Semantics of Intersection Types. In Electronic Proceedings of 3rd International Workshop Intersection Types and Related Systems(ITRS’04), Turku, Finland. 269–270.

[30]

V. Swarup, U. S. Reddy, and E. Ireland. 1991. Assignments for Applicative Languages. In Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings(Lecture Notes in Computer Science, Vol. 523), John Hughes (Ed.). Springer, 192–214. https://doi.org/10.1007/3540543961_10

[31]

J.-P. Talpin and P. Jouvelot. 1994. The Type and Effect Discipline. Inf. Comput. 111, 2 (1994), 245–296. https://doi.org/10.1006/inco.1994.1046

Digital Library

[32]

M. Tofte. 1990. Type Inference for Polymorphic References. Inf. Comput. 89, 1 (1990), 1–34. https://doi.org/10.1016/0890-5401(90)90018-D

Digital Library

[33]

S. van Bakel. 1995. Intersection Type Assignment Systems. Theoretical Computer Science 151, 2 (1995), 385–435.

Digital Library

[34]

P. Wadler. 1992. The Essence of Functional Programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992. ACM Press, 1–14. https://doi.org/10.1145/143165.143169

Digital Library

[35]

P. Wadler. 1995. Monads for Functional Programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques(Lecture Notes in Computer Science, Vol. 925). Springer, 24–52. https://doi.org/10.1007/3-540-59451-5_2

[36]

P. Wadler and P. Thiemann. 2003. The marriage of effects and monads. ACM Trans. Comput. Log. 4, 1 (2003), 1–32. https://doi.org/10.1145/601775.601776

Digital Library

[37]

A. K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94. https://doi.org/10.1006/inco.1994.1093

Digital Library

Cited By

Ke WChan K(2021)A Subtyping Scheme for Nominal and Structural Types Based on Class Graph EquivalenceProceedings of the 2021 4th International Conference on Blockchain Technology and Applications10.1145/3510487.3510509(151-157)Online publication date: 17-Dec-2021
https://dl.acm.org/doi/10.1145/3510487.3510509

Index Terms

Intersection types for a λ-calculus with global store
1. Mathematics of computing
2. Software and its engineering

Index terms have been assigned to the content through auto-classification.

Recommendations

A typed lambda calculus with intersection types

Intersection types are well known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical ...
A Typed Lambda Calculus with Gradual Intersection Types
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming

Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their ...
Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '21: Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming

September 2021

277 pages

ISBN:9781450386890

DOI:10.1145/3479394

Copyright © 2021 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 October 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

PPDP 2021

PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming

September 6 - 8, 2021

Tallinn, Estonia

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
62
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ke WChan K(2021)A Subtyping Scheme for Nominal and Structural Types Based on Class Graph EquivalenceProceedings of the 2021 4th International Conference on Blockchain Technology and Applications10.1145/3510487.3510509(151-157)Online publication date: 17-Dec-2021
https://dl.acm.org/doi/10.1145/3510487.3510509

View Options

Get Access

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.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Table of Contents