Abstract is missing.
- Non-linear Pattern Matching with Backtracking for Non-free Data TypesSatoshi Egi, Yuichi Nishiwaki. 3-23 [doi]
- Factoring Derivation Spaces via Intersection TypesPablo Barenbaum, Gonzalo Ciruelos. 24-44 [doi]
- Types of FireballsBeniamino Accattoli, Giulio Guerrieri. 45-66 [doi]
- On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features - A Benchmark and Tool EvaluationLi Sui, Jens Dietrich, Michael Emery, Shawn Rasheed, Amjed Tahir. 69-88 [doi]
- Complexity Analysis of Tree Share StructureXuan Bach Le, Aquinas Hobor, Anthony W. Lin. 89-108 [doi]
- Relational Thread-Modular Abstract Interpretation Under Relaxed Memory ModelsThibault Suzanne, Antoine Miné. 109-128 [doi]
- Scallina: Translating Verified Programs from Coq to ScalaYoussef El Bakouny, Dani Mezher. 131-145 [doi]
- HoIce: An ICE-Based Non-linear Horn Clause SolverAdrien Champion, Naoki Kobayashi 0001, Ryosuke Sato. 146-156 [doi]
- Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof GeneralHideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka. 157-165 [doi]
- The Practice of a Compositional Functional Programming LanguageTimothy Jones 0002, Michael Homer. 166-177 [doi]
- New Approaches for Almost-Sure Termination of Probabilistic ProgramsMingzhang Huang, Hongfei Fu, Krishnendu Chatterjee. 181-201 [doi]
- Particle-Style Geometry of Interaction as a Module SystemUlrich Schöpp. 202-222 [doi]
- Automated Synthesis of Functional Programs with Auxiliary FunctionsShingo Eguchi, Naoki Kobayashi 0001, Takeshi Tsukada. 223-241 [doi]
- Modular Verification of SPARCv8 CodeJunpeng Zha, Xinyu Feng, Lei Qiao. 245-263 [doi]
- Formal Small-Step Verification of a Call-by-Value Lambda Calculus MachineFabian Kunze, Gert Smolka, Yannick Forster 0002. 264-283 [doi]
- Automated Modular Verification for Relaxed Communication ProtocolsAndreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun. 284-305 [doi]
- Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural NetworksTaro Sekiyama, Kohei Suenaga. 309-328 [doi]
- On the Complexity of Pointer Arithmetic in Separation LogicJames Brotherston, Max I. Kanovich. 329-349 [doi]
- A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length ConstraintsQuang Loc Le, Mengda He. 350-372 [doi]
- Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOASUrara Yamada, Kenichi Asai. 375-393 [doi]
- Model Checking Differentially Private PropertiesDepeng Liu, Bow-Yaw Wang, Lijun Zhang. 394-414 [doi]
- Shallow Effect HandlersDaniel Hillerström, Sam Lindley. 415-435 [doi]