Wed 18 Jan 2023 18:00 - 19:30 at Grand Ballroom A - SRC Poster Chair(s): Jeehoon Kang, Danfeng Zhang

Choreographic programming is an emerging programming paradigm for writing distributed programs. Instead of writing code individually for each node in a distributed system and then assembling them together—which could lead to errors like deadlocks due to mismatches between sends and receives—choreographic programming allows writing a single program (called a choreography) that describes the behavior of the whole system and then automatically generating code for each node via a technique called endpoint projection. By having a global view of message communication, choreographic programming not only provides an integrated way to write distributed programs, but also guarantees deadlock freedom by design.

Although previous work on choreographic programming has developed its metatheory substantially, a practical implementation is still lacking, especially in the context of functional programming. In this paper, we present HasChor, a domain-specific language in Haskell for choreographic programming. HasChor provides users with a monad for writing choreographies and an endpoint projection function for translating a choreography to equivalent concurrent programs. We hope HasChor can serve as a platform for future research into functional choreographic programming and help its adaption in the real world.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

18:00 - 19:30
SRC PosterStudent Research Competition at Grand Ballroom A
Chair(s): Jeehoon Kang KAIST, Danfeng Zhang Pennsylvania State University
18:00
90m
Talk
Zydeco: A Stack-Based Call-By-Push-Value Language
Student Research Competition
Yuchen Jiang University of Michigan, Runze Xue CSE Department at the University of Michigan
18:00
90m
Talk
HasChor: Choreographic Programming in Haskell
Student Research Competition
Gan Shen University of California, Santa Cruz, USA
18:00
90m
Talk
Towards Synthesis in Superposition
Student Research Competition
18:00
90m
Talk
A Formalization of Observational Equivalence in Message Passing Protocols
Student Research Competition
Nathan Liittschwager University of California, Santa Cruz
18:00
90m
Talk
On the metatheory of IRs and the CPS-calculus
Student Research Competition
Paulo Torrens University of Kent
18:00
90m
Talk
Scalable Synthesis of Regular Expressions From Only Positive Examples
Student Research Competition
18:00
90m
Talk
Evaluating Soundness of a Gradual Verifier with Property Based Testing
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
18:00
90m
Talk
A mechanized model for logical clocks
Student Research Competition
Jonathan Castello UC Santa Cruz
18:00
90m
Talk
Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Student Research Competition
Joshua Turcotti Cornell University
18:00
90m
Talk
Synthesizing Vectorized Code via Verified Lifting
Student Research Competition
Jeremy Ferguson University of California-Berkeley
18:00
90m
Talk
Citrus: A Dependently Typed Framework for Pulse-Based Logic
Student Research Competition
Harlan Kringen UC Santa Barbara, Ben Hardekopf University of California at Santa Barbara
18:00
90m
Talk
Neko: A quantum map-filter-reduce programming language
Student Research Competition
Elton Pinto Georgia Institute of Technology
18:00
90m
Talk
Compiling and Running High-level Quantum Programs
Student Research Competition
18:00
90m
Talk
Trace-Guided Inductive Synthesis of Recursive Functional Programs
Student Research Competition
Yongwei Yuan Purdue University