Translating Concepts of the Futhark Programming Language into an Extended Pi-Calculus
summary
Translate a simplified Futhark-like language ButF into a Pi-calculus extended with broadcasting and labelled names, implement arrays as a network of persistent cell structures with handle-based servers, and add a repeat synchronization to emulate call-by-value. The translation proves operational correspondence (sound and complete), annotates processes with a cost model, and gives an asymptotic complexity comparison to Futhark; many administrative communications are needed and the replication-heavy encoding works but raises performance and evaluation-order concerns.
AI-written summary · about
chapters (11)
- 0:00Project introduction
- 1:14Pi-calculus overview
- 4:48Basic Futhark model
- 7:22Extending Pi-calculus
- 8:25Translation approach
- 10:11Arrays with persistent cells
- 12:23Call-by-value semantics
- 13:46Proving correctness
- 16:14Conclusion
- 16:37Future work
- 18:24Q&A
related talks
01h 01mLive Lambda Calculus
25mFormalizing pi-Calculus in Guarded Cubical Agda
23mTermination Analysis for the pi-Calculus by Reduction to Sequential Program Termination
41mAn Introduction to Functional Imperative Programming in Flix
26mFusing Session-Typed Concurrent Programming into Functional Programming
18mPipit: Reactive Systems in F★ (Extended Abstract)
13mComputation Focusing
24mA Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F...