publish 10(3)

Author: krono

2025/10/19/index.markdown

@@ -21,6 +21,8 @@ authors:
     affiliation: "University of Tübingen, Germany"
     id: "0000-0001-8709-6321"
 
+arxiv: "2511.15819"
+file: "https://arxiv.org/pdf/2511.15819v1.pdf"
 excerpt: "The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new **operations**, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new **constructors**, such as by adding a new object implementing an interface in object-oriented programming. Most dependently typed languages have good support for the former style through **inductive** types, but support for the latter style through **coinductive** types is usually much poorer. Polarity is a language that treats both kinds of types symmetrically and allows the developer to switch between type representations.However, it currently lacks several features expected of a state-of-the-art dependently typed language, such as implicit arguments. The central aim of this paper is to provide an algorithmic type system and inference algorithm for implicit arguments that respect the core symmetry of the language. Our work provides two key contributions: a complete algorithmic description of the type system backing Polarity, and a comprehensive description of a unification algorithm that covers arbitrary inductive and coinductive types. We give rules for reduction semantics, conversion checking, and a unification algorithm for pattern-matching, which are essential for a usable implementation. A work-in-progress implementation of the algorithms in this paper is available at [polarity-lang.github.io](https://polarity-lang.github.io/). We expect that the comprehensive account of the unification algorithm and our design decisions can serve as a blueprint for other dependently typed languages that support inductive and coinductive types symmetrically."
 ---
 Bohdan Liesnikov[^1] [![OrcidLogo]](https://orcid.org/0009-0000-2216-8830), David Binder[^2] [![OrcidLogo]](https://orcid.org/0000-0003-1272-0972), and Tim Süberkrüb[^3] [![OrcidLogo]](https://orcid.org/0000-0001-8709-6321)
@@ -30,7 +32,7 @@ The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 3, Articl
 Submission date: 2025-06-02  
 Publication date: 2025-10-15  
 DOI: <https://doi.org/10.22152/programming-journal.org/2025/10/19>  
-Full text: *t.b.a*  
+Full text: [PDF](https://arxiv.org/pdf/2511.15819v1.pdf)  
 
 
 ### Abstract

2025/10/20/index.markdown

@@ -17,6 +17,8 @@ authors:
     affiliation: "University of Utah, USA"
     id: "0000-0001-7078-9287"
 
+arxiv: "2511.15820"
+file: "https://arxiv.org/pdf/2511.15820v1.pdf"
 excerpt: "We built Chorex, a language that brings choreographic programming to Elixir as a path toward robust distributed applications. Chorex is unique among choreographic languages because it tolerates failure among actors: when an actor crashes, Chorex spawns a new process, restores state using a checkpoint, and updates the network configuration for all actors. Chorex also proves that full-featured choreographies can be implemented via metaprogramming, and that doing so achieves tight integration with the host language. For example, mismatches between choreography requirements and an actor implementation are reported statically and in terms of source code rather than macro-expanded code. This paper illustrates Chorex on several examples, ranging from a higher-order bookseller to a secure remote password protocol, details its implementation, and measures the overhead of checkpointing. We conjecture that Chorex’s projection strategy, which outputs sets of stateless functions, is a viable approach for other languages to support restartable actors."
 ---
 Ashton Wiersdorf[^1] [![OrcidLogo]](https://orcid.org/0000-0001-5524-7930) and Ben Greenman[^2] [![OrcidLogo]](https://orcid.org/0000-0001-7078-9287)
@@ -26,7 +28,7 @@ The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 3, Articl
 Submission date: 2025-06-01  
 Publication date: 2025-10-15  
 DOI: <https://doi.org/10.22152/programming-journal.org/2025/10/20>  
-Full text: *t.b.a*  
+Full text: [PDF](https://arxiv.org/pdf/2511.15820v1.pdf)  
 
 
 ### Abstract

2025/10/21/index.markdown

@@ -21,6 +21,8 @@ authors:
     affiliation: "University of Tokyo, Tokyo, Japan"
     id: "0000-0002-1058-5941"
 
+arxiv: "2511.15821"
+file: "https://arxiv.org/pdf/2511.15821v1.pdf"
 excerpt: |
     Virtual machines (VMs) are highly beneficial for microcontroller development. 
     In particular, interactive programming environments greatly facilitate iterative development processes, 
@@ -50,7 +52,7 @@ The Art, Science, and Engineering of Programming, 2025, Vol. 10, Issue 3, Articl
 Submission date: 2025-06-02  
 Publication date: 2025-10-15  
 DOI: <https://doi.org/10.22152/programming-journal.org/2025/10/21>  
-Full text: *t.b.a*  
+Full text: [PDF](https://arxiv.org/pdf/2511.15821v1.pdf)  
 
 
 ### Abstract

2025/10/index.markdown

@@ -2,6 +2,7 @@
 title: "Volume 10"
 type: "volume"
 id: "urn:doi:10.22152%2Fprogramming-journal.org%2F2025%2F10"
+date: "2025-02-28"
 ---
 DOI: <https://doi.org/10.22152/programming-journal.org/2025/10>
 
@@ -60,6 +61,21 @@ Chinmayi Prabhu Baramashetru, Paola Giannini, Silvia Lizeth Tapia Tarifa, and Ol
 
 
 
+* [Volume 10, Issue 3](issue3)  
+
+
+
+
+  {: start="19"}
+  1. [Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments](/2025/10/19)  
+Bohdan Liesnikov, David Binder, and Tim Süberkrüb
+  1. [Chorex: Restartable, Language-Integrated Choreographies](/2025/10/20)  
+Ashton Wiersdorf and Ben Greenman
+  1. [BlueScript: A Disaggregated Virtual Machine for Microcontrollers](/2025/10/21)  
+Fumika Mochizuki, Tetsuro Yamazaki, and Shigeru Chiba
+
+
+
 
 
 

2025/10/issue3/index.markdown

@@ -4,7 +4,7 @@ category: "Issues"
 order: -10003
 type: "issue"
 id: "urn:doi:10.22152%2Fprogramming-journal.org%2F2025%2F10%2Fissue3"
-date: "2025-11-19"
+date: "2025-11-21"
 ---
 DOI: <https://doi.org/10.22152/programming-journal.org/2025/10/issue3>