A Self-Dual Distillation of Session Types (Pearl)VCOOP 2022ECOOP 2022
Thu 16 Jun 2022 17:45 - 18:15 at Zoom - VCOOP 2 Chair(s): Sophia Drossopoulou
We introduce ƛ (“lambda-barrier”), a minimal extension of linear λ-calculus with concurrent communication, which adds only a single new fork
construct for spawning threads. It is inspired by GV, a session-typed functional language that is also based on linear λ-calculus. Unlike GV, ƛ strives to be as simple as possible, and adds no new operations other than fork
, no new type formers, and no explicit definition of session type duality. Instead, we use the linear function type τ₁ → τ₂ for communication between threads, which is dual to τ₂ → τ₁, i.e. the function type constructor is dual to itself. Nevertheless, we can encode session types as ƛ types, GV’s channel operations as ƛ terms, and show that this encoding is type-preserving. The linear type system of ƛ ensures that all programs are deadlock-free and satisfy global progress, which we prove in Coq. Because of ƛ’s minimality, these proofs are simpler and shorter than mechanized proofs of deadlock freedom for GV.
Thu 9 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 16 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 18:15 | |||
16:45 30mTalk | Direct Foundations for Compositional ProgrammingVCOOP 2022 Research Papers Andong Fan Zhejiang University, Xuejing Huang The University of Hong Kong, Han Xu Peking University, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong Pre-print Media Attached | ||
17:15 30mTalk | Experience: Model-Based Feedback-Driven Greybox Fuzzing for Web ApplicationsVCOOP 2022 Research Papers François Gauthier Oracle Labs, Behnaz Hassanshahi Oracle Labs, Australia, Benjamin Selwyn-Smith Oracle Labs, Trong Nhan Mai Oracle Labs, Max Schlüter Oracle Labs, Micah Williams Oracle | ||
17:45 30mTalk | A Self-Dual Distillation of Session Types (Pearl)VCOOP 2022ECOOP 2022 Research Papers Jules Jacobs Radboud University Nijmegen Pre-print |