Programming Languages and Systems

Abstract

Program Verification Time Credits and Time Receipts in Iris . Meta-FI: Proof Automation with SMT, Tactics, and Metaprograms. Semi-automated Reasoning About Non-determinism in C Expressions. Language Design Codata in Action. Composing Bidirectional Programs Monadically. Program Semantics, Extended call-by-push-value: Reasoning About Effectful Programs and Evaluation Order. Types Handling Polymorphic Algebraic Effects. Security and Incremental Computation Robustly Safe Compilation. Concurrency and Distribution Asynchronous Timed Session Types: From Duality to Time-Sensitive Processes. Program Analysis and Automated Verification Data Races and Static Analysis for Interrupt-Driven Kernels.