ESOP 2024
30 papers
- A Denotational Approach to Release/Acquire Concurrency
- A Formal Treatment of Bidirectional Typing
- A Modular Soundness Theory for the Blackboard Analysis Architecture
- Artifact Description - Definitional Functoriality for Dependent (Sub)Types
- Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency
- Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence
- Artifact report: Generic bidirectional typing for dependent type theories
- Circuit Width Estimation via Effect Typing and Linear Dependency
- Deciding Subtyping for Asynchronous Multiparty Sessions
- Definitional Functoriality for Dependent (Sub)Types
- Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation
- Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping
- Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
- Generic bidirectional typing for dependent type theories
- Higher-Order LCTRSs and Their Termination
- Hyperproperty Verification as CHC Satisfiability
- Intel PMDK Transactions: Specification, Validation and Concurrency
- Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis
- Maximal Quantified Precondition Synthesis for Linear Array Loops
- Monadic Intersection Types, Relationally
- Observational Equality Meets CIC
- On the Hardness of Analyzing Quantum Programs Quantitatively
- Program Synthesis from Graded Types
- Reconciling Partial and Local Invertibility
- Scoped Effects as Parameterized Algebraic Theories
- Specifying and Verifying Persistent Libraries
- Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
- The Session Abstract Machine
- Trocq: Proof Transfer for Free, With or Without Univalence
- Verified Inlining and Specialisation for PureCake