5 papers · 1 filter
On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values
Simon Daniel, Timon Böhler, David Richter +2
With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure…
Mechanizing Choreographic Programs and Hoare Logic with State Transformers
Timon Böhler, Simon Daniel, David Richter +2
Choreographic programming is a programming model for developing distributed applications where an entire communication protocol is written as a single program, which a compiler the…
DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
Timon Böhler, Tobias Reinhard, David Richter +1
Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive sp…
Compiling with Arrays
David Richter, Timon Böhler, Pascal Weisenburger +1
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and r…
Using Rewrite Strategies for Efficient Functional Automatic Differentiation
Timon Böhler, David Richter, Mira Mezini
Automatic Differentiation (AD) has become a dominant technique in ML. AD frameworks have first been implemented for imperative languages using tapes. Meanwhile, functional implemen…