PPDP 2023
who it's for
programming language researchers, type system designers, formal methods researchers, concurrency and session-type researchers, security and information-flow engineers, compiler engineers, database and query-language researchers
topics
labeled effect handlers; labeled delimited control; finite-map query shredding to SQL; Coq formalized x86 assembler; constant-time program transformation; value-dependent confidentiality labels; multiparty session composition; polymorphic typestate for sessions; abstract-closure closure conversion; graded comonadic cellular automata; intuitionistic metric temporal logic; stable-models integration with miniKanren
| title | author | length |
|---|---|---|
| A Calculus of Delayed Reductions | Steffen van Bakel, Nicolas Wu, Emma Tye | 32m |
Introduce the Calculus of Delayed Reductions (CDR) that tweaks CBPV: forcing only variables, thunking only non-forced computations, and a new substitution that… | ||
| Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operat... | Kazuki Ikemori, Youyou Cong, Hidehiko Masuhara | 24m |
Formalizes four calculi (effect handlers vs delimited-control, static vs generative labels), gives a concrete type system for each and proves type soundness… | ||
| Comprehending queries over finite maps | Wilmer Ricciotti | 35m |
Extends the nested relational calculus with first-class finite maps, grouping, lookups and group-wise aggregation and proves strong normalization, producing… | ||
| 10-Year Most Influential Paper Talk: Coq: the world's best macro assembler? | Andrew Kennedy, Nick Benton, Jonas Jensen, Pierre-Evariste Dagand | 54m |
Ten years ago a Coq formalization models a subset of 32-bit x86 with executable bit/byte memory, an assembler written in Coq that assembles assembly notation… | ||
| Type-directed Program Transformation for Constant-Time Enforcement | Gautier Raimondi, Frédéric Besson, Thomas P. Jensen | 28m |
Claims a relaxed information-flow type that distinguishes direct vs indirect flows and proves any program typable under it can be automatically transformed… | ||
| Data-Dependent Confidentiality in DCR Graphs | Eduardo Geraldo, João Costa Seco, Thomas T. Hildebrandt | 33m |
DCRSec implements a runtime information-flow monitor over Dynamic Condition Response graphs, uses value-dependent labels and a powerset lattice to give… | ||
| Multicompatibility for Multiparty-Session Composition | Franco Barbanera, Mariangiola Dezani, Lorenzo Gheri, Nobuko Yoshida | 32m |
Defines a conservative, flexible method to compose many concurrent systems at once by treating chosen participants as forwarder gateways and encoding… | ||
| Termination in Concurrency, Revisited | Joseph Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez | 31m |
Compares three session-typed termination disciplines by building compositional encodings of processes and types into a Vasconcelos-style baseline, formalizing… | ||
| Polymorphic Typestate for Session Types | Hannes Saffrich, Peter Thiemann | 21m |
Claims that a typestate-based model, using PolyVGR with higher-order polymorphism and existential types, matches the expressivity of functional and linear… | ||
| Strongly-Typed Multi-View Stack-Based Computations | Pieter Koopman, Mart Lubbers | 35m |
A DSL embedded in a strongly typed functional host uses heterogeneous lists to statically ensure required stack arguments are present and that untouched tail… | ||
| Closure Conversion in Little Pieces | Zachary Sullivan, Paul Downen, Zena M. Ariola | 29m |
The paper makes closure conversion a syntactic equality by adding abstract closures to a CBPV-style IL, proving an equational theory sound and complete with… | ||
| Additive Cellular Automata Graded-Monadically | Silvio Capobianco, Tarmo Uustalu | 34m |
Shows that cellular automata are graded comonadic by grading with finite neighborhoods (preordered monoid of subsets) and models uniform continuity via locally… | ||
| Intuitionistic Metric Temporal Logic | Luiz de Sá, Bernardo Toninho, Frank Pfenning | 27m |
Defines Intuitionistic Metric Temporal Logic (IMTL) that extends intuitionistic temporal calculi to dense time with explicit intervals and gives every proof a… | ||
| stablekanren: Integrating Stable Model Semantics with miniKanren | Xiangyu Guo, James Smith, Ajay Bansal | 33m |
StableKanren implements stable model semantics inside miniKanren (Scheme) by compiling normal logic programs into complemented goals and weaving runtime… | ||
| nothing matches | ||