000231867 001__ 231867
000231867 005__ 20190317000844.0
000231867 037__ $$aCONF
000231867 245__ $$aMonotonicity Types
000231867 269__ $$a2017
000231867 260__ $$c2017
000231867 336__ $$aConference Papers
000231867 520__ $$aIn the face of the increasing trend in application development to interact with more and more remote services, and cognizant of the fact that issues arising from data consistency and task coordination are core challenges in distributed programming, the systems and data management communities have taken a keen interest in developing eventually consistent coordination-free models of distributed programming. These efforts have a striking similarity; they can all be characterized by the use of monotone functions as fundamental primitives of composition as well as the monotonic evolution of data over time. Yet, ensuring that application code conforms to the monotonicity constraints of these programming models is a tricky and manual affair, without support from the underlying language or system. In this paper, we present Monotonicity Types, a language and type system for proving functions monotone, which we believe could enable the customization and extension of this class of distributed programming models. We provide a full formalization of Monotonicity Types, including a novel operational semantics oriented from the perspective inside of a function, as well as a type soundness proof using logical relations.
000231867 6531_ $$aCRDTs
000231867 6531_ $$aeventual consistency
000231867 6531_ $$adistributed computing
000231867 6531_ $$aconcurrency
000231867 6531_ $$atypes
000231867 700__ $$aClancy, Kevin
000231867 700__ $$0242185$$g191683$$aMiller, Heather
000231867 700__ $$aMeiklejohn, Christopher
000231867 8564_ $$uhttps://infoscience.epfl.ch/record/231867/files/monotonicity-types.pdf$$zPreprint$$s362026$$yPreprint
000231867 909C0 $$xU10409$$0252187$$pLAMP
000231867 909CO $$qGLOBAL_SET$$pconf$$ooai:infoscience.tind.io:231867$$pIC
000231867 917Z8 $$x191683
000231867 937__ $$aEPFL-CONF-231867
000231867 973__ $$rREVIEWED$$sSUBMITTED$$aEPFL
000231867 980__ $$aCONF