POPL 2025
2025-01-19..2025-01-25
Denver, United States
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
as the organisers put it
Welcome to the website of the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025). POPL 2025 will take place in Denver, Colorado. See the Call For Paper for detailed information. The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, ...
who it's for
programming language researchers, formal methods researchers, compiler developers, verification engineers, proof assistant developers, security researchers, quantum programming language researchers, systems verification engineers
topics
typed structure editors; mixed-size C/C++ model checking; affine quantum type systems; algebraic abstract interpretation; lifting Spectre mitigation proofs; sort polymorphism for Coq; speculative execution noninterference; automated tensor graph verification; linearizability under relaxed memory; iso-recursive subtyping algorithms; dependent type meta-programming; probabilistic relational Hoare logic
| title | author | length |
|---|---|---|
| Pantograph: A Fluid and Typed Structure Editor | Jacob Prinz, Henry Blanchette, Leonidas Lampropoulos | 19m |
Pantograph implements a structure editor that keeps programs as typing derivations by combining tree selection (one-hole contexts for cut/paste and reordering)… | ||
| Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages | Andrea Colledan, Ugo Dal Lago | 19m |
Introduces a type-and-effect system for Quipper that produces parametric upper bounds on circuit size (width, gate count, and wire-level depth) by combining… | ||
| Model Checking C/C++ with Mixed-Size Accesses | Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis | 21m |
Presents an algorithm that lets a DPOR-based model checker handle C/C++ mixed-size accesses by treating whole instructions atomically while allowing revisits… | ||
| Algebras for Deterministic Computation are Inherently Incomplete | Balder ten Cate, Tobias Kapp e9 | 20m |
Claim: the deterministic fragment of Kleene Algebra with Tests (KAT) cannot be generated by any finite set of regular control-flow operators. The proof… | ||
| Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime | Kengo Hirata, Chris Heunen | 21m |
Extends Rust’s type system with sharp α types so qubits are lifetime-annotated dropable qubits (affine inside a lifetime, linear outside), gives two… | ||
| A Taxonomy of Hoare-Like Logics | Lena Verscht, Benjamin Lucien Kaminski | 20m |
Classifies Hoare-like logics by giving a lattice of exact implications between transformers built from predicate transformers and a Kleene-algebra variant… | ||
| Calculational Design of Hyperlogics by Abstract Interpretation | Patrick Cousot, Jeffery Wang | 21m |
Claims a calculational pipeline that starts from an algebraic semantics and builds a structural fixpoint abstract interpreter parameterized by algebraic… | ||
| Fulminate: Testing CN Separation-Logic Specifications in C | Rini Banerjee, Kayvan Memarian, Dhruv C. Makwana, Christopher Pulte, Neel Krishnaswami, Peter Sewell | 20m |
Fulminate translates CN separation-logic annotations into executable C checks that enforce ownership ghost state and explicit ownership transfer at runtime… | ||
| Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks | Xaver Fabian, Marco Patrignani, Marco Guarnieri, Michael Backes | 19m |
Paper introduces a lifting framework that upgrades compiler guarantees proved for weaker speculative semantics to stronger ones without redoing full secure… | ||
| QuickSub: Efficient Iso-Recursive Subtyping | Litao Zhou | 20m |
QuickSub is an algorithm for iso-recursive subtyping that is equivalent to the Amber rules but avoids renaming, unfolding and backtracking by tracking polarity… | ||
| All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants | Josselin Poiret, Gaetan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter | 20m |
Adds a principled sort quantifier that generalizes Prop, Type, and SProp and is implemented in Coq with a new sort-polymorphic prelude that replaces duplicated… | ||
| The Best of Abstract Interpretations | Roberto Giacobazzi, Francesco Ranzato | 24m |
Characterizes when an inductive abstract interpretation equals the abstraction of the concrete semantics, proves that for any non‑trivial abstract domain the… | ||
| Invited Talk: Welcome to Quantum 3.0! | Jens Palsberg | 01h 01m |
Claims that 2024 experiments achieve small but real error suppression (logical error ≈ 0.1% logical error) and that current work produces only a few logical… | ||
| Data Race Freedom à la Mode | Aina Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer | 20m |
DRFcaml extends OCaml's type system with new mode axes (contention and portability) to statically guarantee data-race freedom for multi-threaded OCaml while… | ||
| Avoiding signature avoidance in ML modules with zippers | Clément Blaudeau, Didier Rémy, Gabriel Radanne | 21m |
ZipML presents a path-based type system that prevents signature avoidance by adding floating fields—hidden signature fields represented as zippers—and four… | ||
| Generically Automating Separation Logic by Functors, Homomorphisms, and Modules | Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, Yang Liu | 20m |
Claims a generic theory that generates separation logic reasoning rules from algebraic signatures (functors, homomorphisms, modules) and a compositional… | ||
| SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations | Sören van der Wall, Roland Meyer | 22m |
Introduces a speculative semantics that models attacker-controlled microarchitectural directives and leakage and proves a proof method (a new simulation… | ||
| Welcome from the general chair | Steve Zdancewic | 07m |
Conference runs with three colocated symposia, nine workshops and five tutorials, plus many student and social events; reception at 6:00, SRC poster session… | ||
| Inference Plans for Hybrid Particle Filtering | Ellie Y. Cheng, Eric Atkinson, Guillaume Baudart, Louis Mandel, Michael Carbin | 19m |
Built Siren, a probabilistic programming language that accepts inference plan annotations to force hybrid particle filtering to keep some random variables… | ||
| Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning | Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan | 22m |
Bluebell is a program logic that unifies unary and relational proofs by adding a joint conditioning modality that encodes conditional independence and… | ||
| Coinductive Proofs for Temporal Hyperliveness | Arthur Correnson, Bernd Finkbeiner | 20m |
Framework shows that every forall∃ψ hyperproperty with ψ a safety relation admits a coinductive approximation, enabling incremental witness construction via… | ||
| Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting | Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, Taeyoung Yoon, Youngju Song, Chung-Kil Hur | 21m |
Archmage defines a memory model that uses lazy valuation for int→ptr casts so the integer keeps its value until a pointer interpretation is required, allowing… | ||
| Dis/Equality Graphs | George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, Guido Salvaneschi | 20m |
The paper develops an abstract, extensible framework that proves e-graphs encode the smallest reflexive, symmetric, transitive, congruent closure and adds… | ||
| Progressful Interpreters for Efficient WebAssembly Mechanisation | Xiaojia Rao, Stefan Radziuk, Conrad Watt, Philippa Gardner | 19m |
Implements a progressful interpreter in Coq that uses dependent types to certify both soundness and progress, and extracts an executable with proofs erasable… | ||
| Unifying compositional verification and certified compilation with a three-dimensional(…) | Yu Zhang, Jérémie Koenig, Zhong Shao, Yuting Wang | 20m |
A concrete claim: a three-dimensional algebra of refinement composes module interfaces, abstraction levels, and state views so compiler correctness, linking… | ||
| On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus | Naoki Kobayashi | 19m |
Gives simple proofs that the reachability problem becomes undecidable for four undecidable extensions of finitary PCF and then isolates a decidable fragment… | ||
| CF-GKAT: Efficient Validation of Control-Flow Transformations | Cheng Zhang, Tobias Kappé, David E. Narvàez, Nico Naus | 21m |
Extends GKAT to handle hardcoded indicator variables and non‑local control flow (goto, break, return) and proves sound, complete trace‑equivalence by… | ||
| Consistency of a Dependent Calculus of Indistinguishability | Yiyun Liu, Jonathan Chan, Stephanie Weirich | 20m |
Defines a concrete instance DCOIω with an infinite predicative universe hierarchy and proves logical consistency, strong normalization, and that type… | ||
| Program Analysis via Multiple Context Free Language Reachability | Giovanna Kobus Conrado, Adam Husted Kjelstrøm, Jaco van de Pol, Andreas Pavlogiannis | 18m |
Introduces MCFL reachability as a tunable, decidable underapproximation for interleaved Dyck (context-sensitive) reachability, implements an algorithm with… | ||
| Biparsers: Exact Printing for Data Synchronisation | Ruifeng Xie, Tom Schrijvers, Zhenjiang Hu | 19m |
Claims a first biparser framework that achieves exact-printing with non-injective parsers by treating parser/printer pairs as monadic lenses, proving… | ||
| Program logics à la carte | Max Vistrup, Michael Sammler, Ralf Jung | 21m |
Combines reusable program-logic fragments for language effects (shared state, concurrency, nondeterminism) so logics can be composed rather than rebuilt. Uses… | ||
| Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order(…) | Taro Sekiyama, Hiroshi Unno | 21m |
Proposes algebraic temporal effects: an axiomatized effect algebra plus an R modality for guarded recursive types that stratifies infinite behavior, an effect… | ||
| Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types | Thien Udomsrirungruang, Nobuko Yoshida | 22m |
Compares top-down global-type workflows against bottom-up endpoint inference with concrete algorithms: a new quadratic type-graph subtyping algorithm replacing… | ||
| Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus | Michael D. Adams, Eric Griffis, Thomas J. Porter, Sundara Vishnu Satish, Eric Zhao, Cyrus Omar | 21m |
Paper claims a version-control model that removes patch synthesis and three-way merge by making edits commute: edits become no diff or merge commutative… | ||
| Semantic Logical Relations for Timed Message-Passing Protocols | Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, Lukasz Ziarek | 19m |
Presents a semantic logical relation that proves any well‑typed program inhabits the timed protocol relation (fundamental theorem) and also lets per‑instance… | ||
| Formalising Graph Algorithms with Coinduction | Donnacha Oisín Kidney, Nicolas Wu | 21m |
Formalisation in Cubical Agda treats graphs as coinductive functions V -> Neighbors V where neighbors are monus-weighted neighbors (possibly infinite multisets… | ||
| Tail Modulo Cons, OCaml, and Relational Separation Logic | Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer | 21m |
Implements Tail Modulo Constructor in the OCaml compiler and shows it reliably turns non‑tail List.map‑style definitions into stack‑safe code; proof of… | ||
| An Incremental Algorithm for Algebraic Program Analysis | Chenyu Zhou, Yuzhou Fang, Jingbo Wang, Chao Wang | 19m |
Method builds an API tree data structure that linearizes CFGs so edits map to leaf insert/delete/update and interpretation values are updated by traversing… | ||
| Adversities in Abstract Interpretation - Accommodating Robustness by Abstract(…) | Roberto Giacobazzi, Isabella Mastroeni, Elia Perantoni | 19m |
Presents a formal framework that defines four concrete notions of classifier robustness via abstract interpretation—concrete, abstract robustness… | ||
| Affect: An Affine Type and Effect System | Orpheas van Rooij, Robbert Krebbers | 21m |
Affect introduces Affine types to statically distinguish one-shot versus multi-shot effect continuations, implements a small language called Affect with ML… | ||
| TensorRight: Automated Verification of Tensor Graph Rewrites | Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodík, Amit Sabne, Charith Mendis | 20m |
TensorRight presents an automated verifier that proves tensor-graph rewrites correct for tensors of arbitrary rank and size by encoding rules in a new core… | ||
| Symbolic Automata: omega-Regularity Modulo Theories | Margus Veanes, Thomas Ball, Gabriel Ebner, Ekaterina Zhuchko | 20m |
Generalizes symbolic automata to omega-regular languages by introducing symbolic transition terms and symbolic derivatives, defines Alternating Buchi (ABW_A)… | ||
| Compositional imprecise probability: a solution from graded monads and Markov categories | Jack Liell-Cock, Sam Staton | 18m |
Provides a fully compositional semantic for imprecise probability by naming nondeterministic choices and tracking them with graded monads, giving a… | ||
| Flo: a Semantic Foundation for Progressive Stream Processing | Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, Mae Milano | 17m |
Flo formalizes two semantic guarantees: streaming progress (operators must emit meaningful partial outputs for unbounded inputs) and eager execution (operators… | ||
| Relaxed Memory Concurrency Re-executed | Evgenii Moiseenko, Matteo Meluzzi, Innokentii Meleshchenko, Ivan Kabashnyi, Anton Podkopaev, Soham Chakraborty | 22m |
Proposes XMM, an almost per‑execution semantics that enforces memory consistency by adding an in‑order execute rule and an out‑of‑order reexecute rule that… | ||
| Preservation of speculative constant-time by compilation | Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte | 18m |
Shows that mainstream compilers (GCC -O0/-O1 and Jasmin) can break speculative constant-time by removing or introducing Spectre-v1 leaks, gives concrete… | ||
| Automated Program Refinement: Guide and Verify Code Large Language Model with(…) | Yufan Cai, Zhe Hou, David Sanan, Xiaokun Luan, Yun Lin, Jun Sun, Jin Song Dong | 19m |
A toolchain called Refine4LLM guides GPT-style code models with refinement calculus, generates code, then checks it with SMT/ATP verification (Z3-like solvers)… | ||
| Sound and Complete Proof Rules for Probabilistic Termination | Rupak Majumdar, V.R. Sathiyanarayana | 19m |
Presents sound and relatively complete proof rules for qualitative and quantitative termination of imperative programs with discrete probabilistic choice and… | ||
| Abstract Operational Methods for Call-by-Push-Value | Sergey Goncharov, Stelios Tsampas, Henning Urbat | 25m |
Claims that categorical, higher-order GSOS methods instantiate to call-by-push-value and fine-grain call-by-value to yield modular, language-independent proof… | ||
| A Primal-Dual Perspective on Program Verification Algorithms | Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham | 19m |
Presents a unified algorithmic framework that generalizes Lagrangians to discrete domains (powersets, predicates, ranking functions) and runs an abstract… | ||
| The Duality of λ-Abstraction | Vikraman Choudhury, Simon J. Gay | 19m |
Presents a concrete extension of call‑by‑value simply‑typed lambda calculus with covalues, coabstraction and coapplication, claiming that inserting double… | ||
| Approximate Relational Reasoning for Higher-Order Probabilistic Programs | Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal | 21m |
Describes Approxis, a higher-order separation logic that treats error credits as first-class resources to prove approximate program refinements for an ML-like… | ||
| Reachability Analysis of the Domain Name System | Dhruv Nevatia, Si Liu, David Basin | 18m |
Provides a decision procedure for DNS verification with worst-case complexity 2ExpTime decision procedure, using a concrete-to-abstract homomorphism that… | ||
| Derivative-Guided Symbolic Execution | Yongwei Yuan, Zhe Zhou, Julia Belyakova, Suresh Jagannathan | 20m |
Framework builds a symbolic execution for functional code that calls opaque, effectful libraries, encoding LTLf specs as symbolic finite automata and using… | ||
| Linear and non-linear relational analyses for Quantum Program Optimization | Matthew Amy, Joseph Lunderville | 21m |
Recasts phase folding as an affine relational analysis and implements nonlinear extensions as affine varieties / polynomial ideals with Gröbner-basis… | ||
| Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis | Philippe Heim, Rayna Dimitrova | 19m |
Proposes a monitor with SMT-based invariants that keeps first-order and temporal structure during translation to symbolic games, emits four verdicts… | ||
| Bidirectional Higher-Rank Polymorphism with Intersection and Union Types | Shengyi Jiang, Chen Cui | 19m |
Presents FIU, a bidirectional type system combining higher‑rank polymorphism with intersection and union types, and proves a sound, complete, decidable… | ||
| Invited Talk: Finding Good Programs by Avoiding Bad Ones | Loris D'Antoni | 01h 04m |
Shows that proving unrealizability — certifying that an entire grammar-derived search space contains no correct program — gives a practical pruning primitive… | ||
| Verifying Quantum Circuits with Level-Synchronized Tree Automata | Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai | 20m |
Introduces level-synchronized tree automata that label transitions with joint choices to synchronize different tree branches, enabling a symbolic encoding of… | ||
| Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops | Fabian Zaiser, Andrzej S. Murawski, C.-H. Luke Ong | 20m |
Automated tool Diabolo implements two provable methods: residual mass semantics (fast unrolling upper/lower bounds) and geometric bound semantics (contraction… | ||
| Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with(…) | Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel | 19m |
Provides a semantic criterion that turns inductive rule systems with binders into strengthened induction theorems by modelling relations as Knaster–Tarski… | ||
| Axe 'Em: Eliminating Spurious States with Induction Axioms | Neta Elad, Sharon Shoham | 20m |
First-order abstractions get refined into well-founded or finite-domain semantics by instantiating an induction axiom schema guided by finitely representable… | ||
| The Decision Problem for Regular First Order Theories | Umang Mathur, David Mestel, Mahesh Viswanathan | 20m |
Work shows decidability for satisfiability of regular sets of first‑order formulae hinges on concrete bounds and automata encodings: tree automata represent… | ||
| A Verified Foreign Function Interface Between Coq and C | Joomy Korkut, Kathrin Stark, Andrew W. Appel | 20m |
VeriFFI provides a verified foreign-function interface that translates Coq dependent types and Coq functional models into VST specs so C functions, once proved… | ||
| On Extending Incorrectness Logic with Backwards Reasoning | Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran | 20m |
Extends incorrectness logic with underspecification so postconditions can ignore irrelevant variables, provides a backwards-proof system that produces… | ||
| Formal Foundations for Translational Separation Logic Verifiers | Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller | 21m |
Provides a formal, mechanized framework that proves soundness of translational separation-logic verifiers by defining a core IVL with both operational and… | ||
| Interaction Equivalence | Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni | 20m |
Defines a checker lambda calculus with black/white lambdas and applications, four beta rules, and a deterministic head interaction steps count that ignores… | ||
| Maximal Simplification of Polyhedral Reductions | Louis Narmour, Tomofumi Yuki, Sanjay Rajopadhye | 22m |
Proposes an algorithm that always attains minimal asymptotic complexity for polyhedral commutative reductions by splitting domains and simplifying each piece… | ||
| Automating equational proofs in Dirac notation | Yingte Xu, Gilles Barthe, Li Zhou | 21m |
Proves that Dirac notation’s first-order theory is decidable by reducing formulas to the theory of real closed fields (Tarski) and shows practical equivalence… | ||
| RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and(…) | Ian Erik Varatalu, Margus Veanes, Juhan Ernits | 21m |
RE# is a derivative-based regex engine built on symbolic derivatives that avoids backtracking, adds intersection and complement plus restricted lookarounds… | ||
| A Dependent Type Theory for Meta-programming with Intensional Analysis | Jason Z. S. Hu, Brigitte Pientka | 20m |
Introduces DeLaM, a concrete dependent layered modal type theory that implements three layers (syntax, MLTT, meta) with quoting of open code, composition… | ||
| A Demonic Outcome Logic for Randomized Nondeterminism | Noam Zilberstein, Dexter Kozen, Alexandra Silva, Joseph Tassarotti | 18m |
Introduces Demonic Outcome Logic that models randomized programs with adversarial nondeterminism using the convex power set semantics, proving a distributive… | ||
| Universal Composability is Robust Compilation | Marco Patrignani, Robert Künnemann, Riad S. Wahby, Ethan Cecchetti | 23m |
Paper claims UC security and robust compilation are equivalent under clear axioms and gives a recipe to mechanize UC proofs. It axiomatizes UC semantics, maps… | ||
| Modelling Recursion and Probabilistic Choice in Guarded Type Theory | Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Annebet Zwart, Alejandro Aguirre, Lars Birkedal | 18m |
Paper encodes FPC⊕ (recursive types + probabilistic choice) inside clocked guarded type theory and builds operational and denotational semantics connected by a… | ||
| A modal deconstruction of Löb induction | Daniel Gratzer | 18m |
Derives Löb induction from a small set of modal primitives and univalent foundations, building Gatsby — a guarded dependent type theory that adds one rule… | ||
| BiSikkel: A Multimode Logical Framework in Agda | Joris Ceulemans, Andreas Nuyts, Dominique Devriese | 20m |
Library implements a multimode logical framework (MULF) on top of the existing Sikkel Agda stack, giving a syntactic MST layer, presheaf semantics and a… | ||
| RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency | Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis | 17m |
RELINCHE is a model checker that verifies per-object atomicity plus preserved synchronization under weak memory by establishing refinement between an… | ||
| MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age | Roland Leißa, Marcel Ullrich, Joachim Meyer, Sebastian Hack | 20m |
MimIR is an extensible, higher-order IR whose core is a pure type system based on the calculus of constructions and that lets developers add domain ops as… | ||
| A quantitative probabilistic relational Hoare logic | Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Gregoire | 19m |
eRHL is a program logic whose pre/post-conditions are nonnegative real-valued functions on pairs of states, and it gives upper bounds on expectations… | ||
| Finite-Choice Logic Programming | Chris Martens, Robert J. Simmons, Michael Arntzenius | 20m |
Defines a new semantics that replaces negation with explicit choices, formalizes rules as functions from databases to choice sets, and proves a… | ||
| VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems | Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur | 19m |
VeriRT provides an end-to-end framework that links abstract timed specs to assembly by (1) embedding low-level timing assumptions into operational semantics… | ||
| Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory | Eric Giovannini, Tingting Ding, Max S. New | 20m |
Presents a denotational model of a simple gradually typed lambda calculus built inside guarded type theory, solving the dynamic-type equation with guarded… | ||
| nothing matches | ||