Mon 16 Nov 2020 22:20 - 23:00 at SPLASH-VII - Posters Session 2 Mirror
With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom.
While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain \emph{constraints} on the payload. We introduce \emph{refined multiparty session types (RMPST)}, an extension of MPST, that express data dependent protocols via \emph{refinement types} on the data types.
We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a multiparty protocol description toolchain, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using \emph{refinement-typed} APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing \emph{static} linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naive implementation, while guaranteeing safety properties from the underlying theory.
Mon 16 Nov Times are displayed in time zone: Central Time (US & Canada) change
10:20 - 11:00 | |||
10:20 40mPoster | Resolution as Intersection Subtyping via Modus PonensOOPSLA Posters Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag | ||
10:20 40mPoster | Macros For Domain-Specific LanguagesOOPSLA Posters Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University | ||
10:20 40mPoster | Precise Inference of Expressive Units of Measurement TypesOOPSLA Posters Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo | ||
10:20 40mPoster | Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA Posters Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University | ||
10:20 40mPoster | A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA Posters Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University DOI Pre-print Media Attached File Attached | ||
10:20 40mPoster | Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA Posters Yu WangNanjing University, China, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University | ||
10:20 40mPoster | Statically Verified Refinements for Multiparty ProtocolsOOPSLA Posters Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London | ||
10:20 40mPoster | Towards a Formal Foundation of Intermittent ComputingOOPSLA Posters Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University | ||
10:20 40mPoster | Incremental Predicate Analysis for Regression VerificationOOPSLA Posters | ||
10:20 40mPoster | StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA Posters | ||
10:20 40mPoster | SATUNE: Synthesizing Efficient SAT EncodersOOPSLA Posters Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine | ||
10:20 40mPoster | Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA Posters Steven HoltzenUniversity of California at Los Angeles, Guy Van den BroeckUniversity of California at Los Angeles, Todd MillsteinUniversity of California, Los Angeles | ||
10:20 40mPoster | Certified and Efficient Instruction SchedulingOOPSLA Posters Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG | ||
10:20 40mPoster | Revisiting Iso-Recursive SubtypingOOPSLA Posters Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong | ||
10:20 40mPoster | Guided Linking: Dynamic Linking Without the CostsOOPSLA Posters Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign | ||
10:20 40mPoster | Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA Posters Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin | ||
10:20 40mPoster | CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA Posters Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University |
22:20 - 23:00 | |||
22:20 40mPoster | Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA Posters Yu WangNanjing University, China, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University | ||
22:20 40mPoster | Towards a Formal Foundation of Intermittent ComputingOOPSLA Posters Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University | ||
22:20 40mPoster | StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA Posters | ||
22:20 40mPoster | Incremental Predicate Analysis for Regression VerificationOOPSLA Posters | ||
22:20 40mPoster | SATUNE: Synthesizing Efficient SAT EncodersOOPSLA Posters Hamed GorjiaraUniversity of California at Irvine, Guoqing Harry XuUniversity of California at Los Angeles, Brian DemskyUniversity of California at Irvine | ||
22:20 40mPoster | A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA Posters Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University DOI Pre-print Media Attached File Attached | ||
22:20 40mPoster | Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA Posters Pengyu NieUniversity of Texas at Austin, Marinela ParovicUniversity of Texas at Austin, Zhiqiang ZangUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin, Aleksandar MilicevicMicrosoft, Milos GligoricUniversity of Texas at Austin | ||
22:20 40mPoster | Statically Verified Refinements for Multiparty ProtocolsOOPSLA Posters Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London | ||
22:20 40mPoster | Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA Posters Ruyi JiPeking University, Yican SunPeking University, Yingfei XiongPeking University, Zhenjiang HuPeking University | ||
22:20 40mPoster | Revisiting Iso-Recursive SubtypingOOPSLA Posters Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong | ||
22:20 40mPoster | Macros For Domain-Specific LanguagesOOPSLA Posters Michael BallantyneNortheastern University, Alexis KingNorthwestern University, Matthias FelleisenNortheastern University | ||
22:20 40mPoster | CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA Posters Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University | ||
22:20 40mPoster | Certified and Efficient Instruction SchedulingOOPSLA Posters Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril SixKalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David MonniauxGrenoble Alps University / CNRS / Grenoble INP / VERIMAG | ||
22:20 40mPoster | Resolution as Intersection Subtyping via Modus PonensOOPSLA Posters Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag | ||
22:20 40mPoster | Precise Inference of Expressive Units of Measurement TypesOOPSLA Posters Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo | ||
22:20 40mPoster | Guided Linking: Dynamic Linking Without the CostsOOPSLA Posters Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign | ||
22:20 40mPoster | Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA Posters Steven HoltzenUniversity of California at Los Angeles, Guy Van den BroeckUniversity of California at Los Angeles, Todd MillsteinUniversity of California, Los Angeles |