ICFP 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1230)

A Zain K AamerAamer, Zain K University of PennsylvaniaUnited States Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Neha AbbasAbbas, Neha University of California, Santa Cruz SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Andreas AbelAbel, Andreas Gothenburg UniversitySweden Committee Member in ICFP Programme Committee within the ICFP Papers-track
Pedro AbreuAbreu, Pedro Type Theory Forall Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Coşku AcayAcay, Coşku Observe, Inc.United States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michael D. AdamsAdams, Michael D. National University of SingaporeUnited States Pushing the Information-Theoretic Limits of Random Access Lists
Nicholas AdamsAdams, Nicholas None How to secure a distributed database such as OpenRiak with open-source tools
Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST), Japan A practical formalization of monadic equational reasoning in dependent-type theory
Eddie AftandilianAftandilian, Eddie GitHub NextUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chaitanya AgarwalAgarwal, Chaitanya New York University Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Danel AhmanAhman, Danel University of LjubljanaSlovenia SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Amal AhmedAhmed, Amal Northeastern University, USAUnited States From Linearity to Borrowing
Joongwon AhnAhn, Joongwon Seoul National University React-tRace: A Semantics for Understanding React Hooks
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands Committee Member in Program Committee within the ICFP Student Research Competition-track 2-Functoriality of Initial Semantics, and Applications
Willow AhrensAhrens, Willow Massachusetts Institute of TechnologyUnited States Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Marat AkhinAkhin, Marat JetBrainsNetherlands Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Dependency-Aware Compilation for Surface Code Quantum Architectures Checking Observational Correctness of Database Systems Compiling Quantum Circuits
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference
Mark W. AldrichAldrich, Mark W. Tufts UniversityUnited States RestPi: Path-Sensitive Type Inference for REST APIs
Shan AliAli, Shan Yale University Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Guillaume AllaisAllais, Guillaume University of StrathclydeUnited Kingdom Frex: Dependently Typed Algebraic Simplification Committee Member in ICFP Programme Committee within the ICFP Papers-track
Henry AllardAllard, Henry Iowa State UniversityUnited States Embedding Quantum Program Verification into Dafny
Anders Alnor MathiasenAlnor Mathiasen, Anders Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Dalal AlrajehAlrajeh, Dalal Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Saman AmarasingheAmarasinghe, Saman Massachusetts Institute of TechnologyUnited States Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Yujin AnAn, Yujin Chungnam National University Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability
Zixi AnAn, Zixi Debugging WebAssembly? Put some Whamm on it!
Aditya AnandAnand, Aditya Indian Institute of Technology BombayIndia CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Emmanuel Anaya GonzalezAnaya Gonzalez, Emmanuel UCSD Laurel: Unblocking Automated Verification with Large Language Models
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Sebastian AngelAngel, Sebastian University of PennsylvaniaUnited States Structural temporal logic for mechanized program verification
Anastasios AntoniadisAntoniadis, Anastasios University of Athens, GreeceGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Timos AntonopoulosAntonopoulos, Timos Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Meghana Aparna SistlaAparna Sistla, Meghana The University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
David AponteAponte, David Microsoft SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Vincenzo ArceriArceri, Vincenzo University of Parma, ItalyItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sven ArgoArgo, Sven Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Jaime AriasArias, Jaime CNRS; LIPN; Université Sorbonne Paris NordFrance Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Zena M. AriolaAriola, Zena M. University of OregonUnited States A contextual formalization of structural coinduction
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan OCaml Blockly Session Chair of Morning Paper Session (part of SPLASH -E) Committee Member in Program Commitee within the SPLASH -E-track
Flavio AscariAscari, Flavio University of Pisa Revealing Sources of (Memory) Errors via Backward Analysis
Eric AtkinsonAtkinson, Eric Binghamton University Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track OOPSLA Artifact Awards
Jessy AyalaAyala, Jessy University of California, IrvineUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Pedro Henrique Azevedo de AmorimAzevedo de Amorim, Pedro Henrique Cornell University Denotational Foundations for Expected Cost Analysis
B Timur BabakolBabakol, Timur SUNY Binghamton, USA Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Casper BachBach, Casper University of Southern DenmarkDenmark Language-Parametric Reference Synthesis
Jakub BachurskiBachurski, Jakub University of CambridgeUnited Kingdom Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Thomas BAGRELBAGREL, Thomas Tweag, LORIA/INRIA Destination calculus: A linear λ-calculus for purely functional memory writes
Alexander BaiBai, Alexander New York UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Debugging WebAssembly? Put some Whamm on it! Metamorph: Synthesizing Large Objects from Dafny Specifications
Guangdong BaiBai, Guangdong University of QueenslandAustralia Convex Hull Approximation for Activation Functions
Hrishikesh BalakrishnanBalakrishnan, Hrishikesh University of Illinois Urbana-Champaign FO-Complete Program Verification for Heap Logics
Elisa BaniassadBaniassad, Elisa University of British ColumbiaCanada Committee Member in Program Commitee within the SPLASH -E-track
Peihua BaoBao, Peihua University of Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Yuyan BaoBao, Yuyan Augusta UniversityUnited States Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory Complete the Cycle: Reachability Types with Expressive Cyclic References
Mikhail BarashBarash, Mikhail University of BergenNorway Session Chair of Afternoon Paper Session 2 (part of SPLASH -E) Involving Students in Design and Implementation of ECMAScript (JavaScript) Proposals
Celeste BarnabyBarnaby, Celeste University of Texas at AustinUnited States Active Learning for Neurosymbolic Program Synthesis
Dan BarowyBarowy, Dan Williams CollegeUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Clark BarrettBarrett, Clark Stanford UniversityUnited States Interactive Bit Vector Reasoning using Verified Bitblasting
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Committee Member in ICFP Programme Committee within the ICFP Papers-track
Matteo BassoBasso, Matteo Università della Svizzera italiana (USI) HeapBuffers: Why not just using a binary serialization format for your managed memory? Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Osbert BastaniBastani, Osbert University of PennsylvaniaUnited States Opportunistically Parallel Lambda Calculus Active Learning for Neurosymbolic Program Synthesis
Mark BattyBatty, Mark University of KentUnited Kingdom Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Guillaume BaudartBaudart, Guillaume InriaFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Emilien BauerBauer, Emilien University of Edinburgh Compressed and Parallelized Structured Tensor Algebra
Rohan BavishiBavishi, Rohan AmazonUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Julia BelyakovaBelyakova, Julia Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Aaron BembenekBembenek, Aaron The University of MelbourneAustralia Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can do Better
Dorra Ben KhalifaBen Khalifa, Dorra ENAC - University of ToulouseFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jiří BenešBeneš, Jiří University of Tübingen The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking
Avner BensoussanBensoussan, Avner King's College LondonUnited Kingdom Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Nick BentonBenton, Nick MetaUnited Kingdom Committee Member in Distinguished Papers Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ryan BergerBerger, Ryan Nvidia Translation Validation for LLVM's AArch64 Backend
Simon BerlingerBerlinger, Simon Ulm University, Germany Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Jean-Philippe BernardyBernardy, Jean-Philippe University of Gothenburg, Sweden Domain-specific tensor languages Committee Member in ICFP Programme Committee within the ICFP Papers-track
Quentin BernetBernet, Quentin EPFL Logically Qualified Types for Scala
Gilbert BernsteinBernstein, Gilbert University of WashingtonUnited States Polynomial-Time Program Equivalence for Machine Knitting
Ivan BeschastnikhBeschastnikh, Ivan The University of British ColumbiaCanada TraceLinking Implementations with their Verified Designs
Raven BeutnerBeutner, Raven CISPA Helmholtz Center for Information Security, Germany Verifying Asynchronous Hyperproperties in Reactive Systems
Siddharth BhatBhat, Siddharth University of Cambridge Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting
Bishnu BhusalBhusal, Bishnu University of MissouriUnited States Checking $\delta$-Satisfiability of Reals with Integrals
Baldip BijlaniBijlani, Baldip Indian Institute of Technology Kanpur Memory-Safety Verification of Open Programs With Angelic Assumptions
Walter BinderBinder, Walter USI LuganoSwitzerland HeapBuffers: Why not just using a binary serialization format for your managed memory? Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs Reasoning about Weak Isolation Levels in Separation Logic
Stephen M. BlackburnBlackburn, Stephen M. Google; Australian National UniversityAustralia Advancing Performance via a Systematic Application of Research and Industrial Best Practice Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Steve BlackburnBlackburn, Steve Google and Australian National UniversityAustralia Session Chair of Abstraction (part of SPLASH OOPSLA)
Jasmin BlanchetteBlanchette, Jasmin Ludwig-Maximilians-Universität MünchenGermany Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sandrine BlazyBlazy, Sandrine University of RennesFrance Committee Member in Distinguished Papers Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track A Mechanized Semantics for Dataflow Circuits
Andrew BlinnBlinn, Andrew University of MichiganUnited States Syntactic Completions with Material Obligations
Ivana BocevskaBocevska, Ivana TU Wien Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Sean BocirneaBocirnea, Sean University of British Columbia Type-Preserving Flat Closure Optimization
Rastislav BodíkBodík, Rastislav Google Research, Brain TeamUnited States HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
CF Bolz-TereickBolz-Tereick, CF Heinrich-Heine-Universität DüsseldorfGermany Tracing Just-in-time Compilation for Effects and Handlers
Michael D. BondBond, Michael D. Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Daniele BonettaBonetta, Daniele VU AmsterdamNetherlands HeapBuffers: Why not just using a binary serialization format for your managed memory?
Nader Boushehrinejad MoradiBoushehrinejad Moradi, Nader University of UtahUnited States Translation Validation for LLVM's AArch64 Backend
Matt BovelBovel, Matt EPFL Existentialize your Generics Logically Qualified Types for Scala
Wavid BowmanBowman, Wavid University of FloridaUnited States Debugging WebAssembly? Put some Whamm on it!
William J. BowmanBowman, William J. University of British ColumbiaCanada Type Universes as Kripke Worlds Committee Member in ICFP Programme Committee within the ICFP Papers-track Type-Preserving Flat Closure Optimization
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany Committee Member in Program Committee within the ICFP Student Research Competition-track Multiple Resumptions and Local Mutable State, Directly Committee Member in ICFP Programme Committee within the ICFP Papers-track The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking Dynamic Wind for Effect Handlers Tracing Just-in-time Compilation for Effects and Handlers Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation The Simple Essence of Monomorphization
Edwin BradyBrady, Edwin University of St. AndrewsUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Oliver BračevacBračevac, Oliver EPFL, LAMPSwitzerland Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Joachim BreitnerBreitner, Joachim Lean FRO, LLCGermany Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ana BrendelBrendel, Ana University of California Los AngelesUnited States Synthesizing Implication Lemmas for Interactive Theorem Proving
Mitch BrilesBriles, Mitch University of Utah Translation Validation for LLVM's AArch64 Backend
Matthew BrittonBritton, Matthew The Australian National University Verifying Extract Method Refactoring in Rust
Rutger BroekhoffBroekhoff, Rutger Radboud University NijmegenNetherlands Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
Fraser BrownBrown, Fraser CMU Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Roberto BruniBruni, Roberto University of PisaItaly Revealing Sources of (Memory) Errors via Backward Analysis
Anita BuckleyBuckley, Anita USI Lugano A Language for Quantifying Quantum Network Behavior
Humphrey BurchellBurchell, Humphrey University of KentUnited Kingdom Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
William E. ByrdByrd, William E. University of Alabama at BirminghamUnited States Committee Member in Distinguished Papers Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Aurea BíláBílá, Aurea ETH ZurichSwitzerland Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees A Refinement Methodology for Distributed Programs in Rust
Henrik BövingBöving, Henrik Lean FRO Interactive Bit Vector Reasoning using Verified Bitblasting
C Joanna C. S. SantosC. S. Santos, Joanna University of Notre DameUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Cristian CadarCadar, Cristian Imperial College LondonUnited Kingdom P³: Reasoning about Patches via Product Programs
Jessica Belicia CahyonoCahyono, Jessica Belicia Institute of Science TokyoJapan Daisy: An Exercise Environment for Learning Information Modeling
Jose CalderonCalderon, Jose Galois, Inc.United States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
Paulo CanelasCanelas, Paulo Carnegie Mellon UniversityUnited States ROSpec: A Domain-Specific Language for ROS-based Robot Software
Man CaoCao, Man Google Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Cristina CarbunaruCarbunaru, Cristina National University of Singapore, SingaporeSingapore Evolving How We Teach Memory Models
J. CarrCarr, J. University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Chris CasinghinoCasinghino, Chris Jane Street A guided tour through Oxidized OCaml
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université Paris CitéFrance Polymorphic Records for Dynamic Languages
Jonathan CastelloCastello, Jonathan University of California, Santa CruzUnited States CRDT Emulation, Simulation, and Representation Independence Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Gabriele CeciliaCecilia, Gabriele Augusta UniversityItaly Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Sooyoung ChaCha, Sooyoung Sungkyunkwan University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Elena ChachkarovaChachkarova, Elena Kings College London Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Rohit ChadhaChadha, Rohit University of Missouri Checking $\delta$-Satisfiability of Reals with Integrals
Kartik ChandraChandra, Kartik MITUnited States A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder & AmazonUnited States Session Chair of Analysis 1 (part of SPLASH OOPSLA) Bolt-On Strong Consistency: Specification, Implementation, and Verification
Rui ChangChang, Rui Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Prantik ChatterjeeChatterjee, Prantik MathWorksIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Chong ChenChen, Chong Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Dong ChenChen, Dong Huawei Technologies Co., Ltd Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Fei ChenChen, Fei German Research Center for Artificial Intelligence (DFKI), Saarland UniversityGermany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Guanlin ChenChen, Guanlin Peking University Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Hongbo ChenChen, Hongbo Indiana University BloomingtonUnited States Agora: Trust Less and Open More in Verification for Confidential Computing
Hongzheng ChenChen, Hongzheng Cornell UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jiasi ChenChen, Jiasi University of Michigan Hambazi: Spatial Coordination Synthesis for Augmented Reality
Jocelyn Qiaochu ChenChen, Jocelyn Qiaochu New York University, University of AlbertaUnited States Automated Discovery of Tactic Libraries for Interactive Theorem Proving Active Learning for Neurosymbolic Program Synthesis
Junjie ChenChen, Junjie Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure Fuzzing C++ Compilers via Type-Driven Mutation
Mingyi ChenChen, Mingyi University of California, Irvine Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sen ChenChen, Sen Nankai UniversityChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyan ChenChen, Siyan Institute of Computing Technology, Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Tony ChenChen, Tony MIT A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Weiyi ChenChen, Weiyi Purdue University Probabilistic Inference for Datalog with Correlated Inputs
Xi ChenChen, Xi Institute of Computing Technology, Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Yanju ChenChen, Yanju University of California, San DiegoUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yanning ChenChen, Yanning University of Toronto Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Yitong ChenChen, Yitong School of Computer Science and Engineering, College of Software Engineering, School of Artificial Intelligence, Southeast University ABC: Towards a Universal Code Styler through Model Merging
Zhenbang ChenChen, Zhenbang College of Computer, National University of Defense TechnologyChina Multi-Modal Sketch-based Behavior Tree Synthesis
Zhibo ChenChen, Zhibo Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Ellie Y. ChengCheng, Ellie Y. MITUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Feifei ChengCheng, Feifei Iowa State University Embedding Quantum Program Verification into Dafny
Luyu ChengCheng, Luyu Hong Kong University of Science and TechnologyHong Kong SAR China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ruotong ChengCheng, Ruotong University of TorontoCanada Products of Recursive Programs for Hypersafety Verification
Xiao ChengCheng, Xiao Macquarie UniversityAustralia Efficient Abstract Interpretation via Selective Widening
Alvin CheungCheung, Alvin University of California at BerkeleyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tsung-Ju ChiangChiang, Tsung-Ju University of TorontoCanada Multi-stage Programming with Splice Variables
Michele ChiariChiari, Michele TU WienAustria Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Reasoning (part of SPLASH OOPSLA)
Adam ChlipalaChlipala, Adam MIT CSAIL Pyrosome: Verified Compilation for Modular Metatheory
Minki ChoCho, Minki Seoul National UniversitySouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Minsung ChoCho, Minsung United States Scaling Optimization Over Uncertainty via Compilation
Joonwon ChoiChoi, Joonwon Amazon Web ServicesUnited States Revamping Verilog Semantics for Foundational Verification
Eloise ChristianChristian, Eloise Rochester Institute of TechnologyUnited States SIGPLAN AV Report
Ravi ChughChugh, Ravi University of Chicago Code Style Sheets: CSS for Code
Benjamin ChungChung, Benjamin JuliaHub Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Pavel ChuprikovChuprikov, Pavel Télécom Paris, Institut Polytechnique de Paris A Language for Quantifying Quantum Network Behavior
Luisa CicoliniCicolini, Luisa University of CambridgeUnited Kingdom Interactive Bit Vector Reasoning using Verified Bitblasting
Stefan CiobacaCiobaca, Stefan Alexandru Ioan Cuza University of Iasi Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Berk CirisciCirisci, Berk Amazon Web Services UTFix: Change Aware Unit Test Repairing using LLM
Jürgen CitoCito, Jürgen TU WienAustria Static Inference of Regular Grammars for Ad Hoc Parsers
Peter ClarkClark, Peter None How to secure a distributed database such as OpenRiak with open-source tools
Christopher ClarkeClarke, Christopher University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Josh CluneClune, Josh Carnegie Mellon University Interactive Bit Vector Reasoning using Verified Bitblasting
Michael CoblenzCoblenz, Michael University of California, San DiegoUnited States RestPi: Path-Sensitive Type Inference for REST APIs On the Impact of Formal Verification on Software Development An Empirical Evaluation of Property-Based Testing in Python
Tiago CogumbreiroCogumbreiro, Tiago University of Massachusetts BostonUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Albert CohenCohen, Albert Google DeepMindFrance Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Cyril CohenCohen, Cyril Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668France A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Sam CohenCohen, Sam University of Chicago Code Style Sheets: CSS for Code
Youyou CongCong, Youyou Institute of Science TokyoJapan Member at large in Steering Committee for ICFP 2025 An Interactive Learning Environment for Program Design Continuations for All: Language Design Considerations for Accessible Continuations Daisy: An Exercise Environment for Learning Information Modeling
Simon CookseyCooksey, Simon Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Nathan CorbynCorbyn, Nathan University of OxfordUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Arthur CorrensonCorrenson, Arthur CISPA Helmholtz Center for Information SecurityGermany Almost Fair Simulations
Carlos Tome CortinasCortinas, Carlos Tome None Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Nicholas CoughlinCoughlin, Nicholas Defence Science and Technology Group, Australia Translation Validation for LLVM's AArch64 Backend
Aaron CouncilmanCouncilman, Aaron Univ of Illinois Urbana-Champaign FO-Complete Program Verification for Heap Logics
Douglas A. CreagerCreager, Douglas A. AstralUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Will CrichtonCrichton, Will Brown UniversityUnited States A guided tour through Oxidized OCaml
Guofeng CuiCui, Guofeng Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Weidong CuiCui, Weidong Microsoft Research AutoVerus: Automated Proof Generation for Rust Code
D Marcelo d'Amorimd'Amorim, Marcelo North Carolina State UniversityUnited States Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Loris D'AntoniD'Antoni, Loris University of California at San DiegoUnited States LOUD: Synthesizing Strongest and Weakest Specifications Semantics of Sets of Programs Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kyle D. ChinD. Chin, Kyle An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Francesco DagninoDagnino, Francesco Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tim DahmenDahmen, Tim Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Jiarun DaiDai, Jiarun Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ting DaiDai, Ting IBM Research Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ugo Dal LagoDal Lago, Ugo University of Bologna & INRIA Sophia AntipolisItaly Committee Member in ICFP Programme Committee within the ICFP Papers-track On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Jayanaka DantanarayanaDantanarayana, Jayanaka University of MichiganSri Lanka MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Olivier DanvyDanvy, Olivier National University of SingaporeSingapore How Computer Science Was Introduced at Yale-NUS College
David DaraisDarais, David GaloisUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Anupam DasDas, Anupam University of Birmingham, UKUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Markus de Medeirosde Medeiros, Markus New York UniversityUnited States Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Kyle DeedsDeeds, Kyle University of Washington Finch: Sparse and Structured Tensor Programming with Control Flow
Maryam Mehri DehnaviDehnavi, Maryam Mehri University of TorontoCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators KestRel: Relational Verification Using E-Graphs for Program Alignment
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance A Mechanized Semantics for Dataflow Circuits
Brian DemskyDemsky, Brian University of California at Irvine Towards Verifying Crash Consistency
Haotian DengDeng, Haotian Purdue University Complete the Cycle: Reachability Types with Expressive Cyclic References
Ming DengDeng, Ming Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Anoop DeorasDeoras, Anoop AWS AI Labs UTFix: Change Aware Unit Test Repairing using LLM
Farzaneh DerakhshanDerakhshan, Farzaneh Illinois Institute of TechnologyUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Quantified Underapproximation via Labeled Bunches
Ankush DesaiDesai, Ankush Amazon Web ServicesUnited States Checking Observational Correctness of Database Systems
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium Program Chair in Organizing Committee for ICFP 2025 ICFP '25 Program Chair in Steering Committee for ICFP 2025 Session Chair of Distinguished Papers (part of ICFP Papers) PC Chair Report Award Ceremony PC Chair in ICFP Programme Committee within the ICFP Papers-track Session Chair of Wednesday ICFP Keynote (part of ICFP Keynotes)
Samvid DharanikotaDharanikota, Samvid Efficient ComputerUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Adhitha DiasDias, Adhitha Purdue University, USAUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Tomás DiazDiaz, Tomás University of ChileChile Flexible and Expressive Typed Path Patterns for GQL Incremental Certified Programming
Robert DickersonDickerson, Robert Purdue UniversityUnited States KestRel: Relational Verification Using E-Graphs for Program Alignment
Işıl DilligDillig, Işıl University of Texas at AustinUnited States Automated Discovery of Tactic Libraries for Interactive Theorem Proving Probabilistic Inference for Datalog with Correlated Inputs Homomorphism Calculus for User-Defined Aggregations Active Learning for Neurosymbolic Program Synthesis Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimitar DimitrovDimitrov, Dimitar INSAIT, Sofia University "St. Kliment Ohridski"Bulgaria qblaze: An Efficient and Scalable Sparse Quantum Simulator
Christos DimoulasDimoulas, Christos Northwestern UniversityUnited States The Rational Programmer, A Method for Investigating Programming Language Pragmatics Contract System Metatheories à la Carte: A Transition-System View of Contracts Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shuo DingDing, Shuo Georgia Institute of TechnologyChina Fast Constraint Synthesis for C++ Function Templates
Alexander DingesDinges, Alexander RPTU Kaiserslautern-LandauGermany Committee Member in Program Committee within the ICFP Student Research Competition-track Binary search—think positive Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Chandeepa DissanayakeDissanayake, Chandeepa Iowa State UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Stephen DolanDolan, Stephen Jane StreetUnited Kingdom Modal Effect Types
Jin Song DongDong, Jin Song National University of SingaporeSingapore Verification of Bit-Flip Attacks against Quantized Neural Networks
Rui DongDong, Rui University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Maximilian DoréDoré, Maximilian University of Oxford Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
Paul DownenDownen, Paul University of Massachusetts at LowellUnited States A contextual formalization of structural coinduction
Dana Drachsler CohenDrachsler Cohen, Dana TechnionIsrael Quantization with Guaranteed Floating-Point Neural Network Classifications Mini-Batch Robustness Verification of Deep Neural Networks Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Derek DreyerDreyer, Derek MPI-SWSGermany JFP Announcement
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Reasoning about External Calls
Xuan Du TrinhDu Trinh, Xuan Stony Brook UniversityUnited States Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Xiaoning DuDu, Xiaoning Monash UniversityAustralia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yuanlin DuanDuan, Yuanlin Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Christophe DubachDubach, Christophe McGill UniversityCanada Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Gregory J. DuckDuck, Gregory J. National University of SingaporeSingapore Large Language Model powered Symbolic Execution
Léon DucruetDucruet, Léon Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Arpita DuttaDutta, Arpita National University of SingaporeSingapore Incremental and Unbounded Loop Analysis
Saikat DuttaDutta, Saikat Cornell UniversityUnited States Understanding and Improving Flaky Test Classification
E Harley D. Eades IIIEades III, Harley D. Augusta UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Marco EilersEilers, Marco ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Susan EisenbachEisenbach, Susan Imperial College LondonUnited Kingdom Reasoning about External Calls
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Member at large in Steering Committee for ICFP 2025 Session Chair of Type 2 (part of SPLASH OOPSLA) Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track A guided tour through Oxidized OCaml
Martin ElsmanElsman, Martin University of CopenhagenDenmark Session Chair of Applications and SRC Talks (part of ICFP Papers)
Joel S EmerEmer, Joel S MIT/NVIDIAUnited States The Continuous Tensor Abstraction: Where Indices are Real
Constantin EneaEnea, Constantin LIX, CNRS, Ecole Polytechnique Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guilherme EspadaEspada, Guilherme LASIGE, University of LisbonPortugal SIGPLAN AV Report
Patrick EugsterEugster, Patrick USI Lugano, SwitzerlandSwitzerland A Language for Quantifying Quantum Network Behavior
Tae Eun KimEun Kim, Tae KAISTSouth Korea Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Karine Even-MendozaEven-Mendoza, Karine King’s College LondonUnited Kingdom Session Chair of Testing 1 (part of SPLASH OOPSLA) Session Chair of Compilation 2 (part of SPLASH OOPSLA) Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
F Teodoro F. CollinF. Collin, Teodoro MIT CSAIL Finch: Sparse and Structured Tensor Programming with Control Flow The Continuous Tensor Abstraction: Where Indices are Real
Luis F. GomesF. Gomes, Luis Carnegie Mellon UniversityPortugal Student Volunteer Co-Chair in Organizing Committee for ICFP 2025
Chris FallinFallin, Chris F5United States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Max FanFan, Max Cornell University Proof Repair across Quotient Type Equivalences
Le FangFang, Le Purdue University Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Ruijie FangFang, Ruijie University of Texas at AustinUnited States Software Model Checking via Summary-Guided Search Homomorphism Calculus for User-Defined Aggregations
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Products of Recursive Programs for Hypersafety Verification
Aleksandr FedchinFedchin, Aleksandr Tufts UniversityUnited States Metamorph: Synthesizing Large Objects from Dafny Specifications
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Marc FeeleyFeeley, Marc Université de MontréalCanada Float Self-Tagging
Qiong FengFeng, Qiong Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yang FengFeng, Yang Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Yao FengFeng, Yao Tsinghua University Adaptive Shielding via Parametric Safety Proofs
Yu FengFeng, Yu University of California at Santa BarbaraUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Ziyuan FengFeng, Ziyuan Nanjing University of Science and Technology Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Pietro FerraraFerrara, Pietro Ca’ Foscari University of VeniceItaly Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Patrick FerrisFerris, Patrick University of Cambridge, UKUnited Kingdom Functional Networking for Millions of Docker Desktops (Experience Report)
Jack FeserFeser, Jack BasisUnited States Peepco: Batch-Based Consistency Optimization
Jonas FialaFiala, Jonas ETH Zürich Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Andrzej FilinskiFilinski, Andrzej DIKU, University of Copenhagen Committee Member in ICFP Programme Committee within the ICFP Papers-track
Robert Bruce FindlerFindler, Robert Bruce Northwestern UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Contract System Metatheories à la Carte: A Transition-System View of Contracts Metaprogramming in Rhombus
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Almost Fair Simulations Verifying Asynchronous Hyperproperties in Reactive Systems
Patricia FirlejczykFirlejczyk, Patricia ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Emily FirstFirst, Emily University of California, San DiegoUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Matthew FlattFlatt, Matthew University of UtahUnited States Session Chair of Systems (part of SPLASH OOPSLA) Metaprogramming in Rhombus
Krisztian FlautnerFlautner, Krisztian University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Cyril Flurin MoserFlurin Moser, Cyril ETH Zurich Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Alcides FonsecaFonseca, Alcides LASIGE; University of LisbonPortugal ROSpec: A Domain-Specific Language for ROS-based Robot Software
Sophie FortzFortz, Sophie King's College LondonUnited Kingdom Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States Session Chair of Synthesis 2 (part of SPLASH OOPSLA) RestPi: Path-Sensitive Type Inference for REST APIs Metamorph: Synthesizing Large Objects from Dafny Specifications
Nate FosterFoster, Nate Cornell University; Jane StreetUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adrian FrancalanzaFrancalanza, Adrian University of MaltaMalta Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Mario FrankFrank, Mario University of PotsdamGermany Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Michael FranzFranz, Michael University of California, IrvineUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Leon FrenotFrenot, Leon ENS Lyon Interactive Bit Vector Reasoning using Verified Bitblasting
Marco FrigoFrigo, Marco University of Illinois at Urbana-Champaign End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Thomas FritzFritz, Thomas University of ZurichSwitzerland An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Daniel FruminFrumin, Daniel University of GroningenNetherlands Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Structural Abstraction and Refinement for Probabilistic Programs
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States ICFP'24 General Chair in Steering Committee for ICFP 2025
Marcial GaißertGaißert, Marcial University of TübingenGermany Tracing Just-in-time Compilation for Effects and Handlers
Cunyuan GaoGao, Cunyuan HKUST A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference
Miao GaoGao, Miao School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University ABC: Towards a Universal Code Styler through Model Merging
Pengfei GaoGao, Pengfei ByteDance Verification of Bit-Flip Attacks against Quantized Neural Networks
Yanfeng GaoGao, Yanfeng Nanjing University HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Zhiqiang GaoGao, Zhiqiang School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University ABC: Towards a Universal Code Styler through Model Merging
Andrés M. GarcedGarced, Andrés M. Seton Hall University Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Ronald GarciaGarcia, Ronald University of British ColumbiaCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Deepak GargGarg, Deepak MPI-SWSGermany Fusing Session-Typed Concurrent Programming into Functional Programming Committee Member in ICFP Programme Committee within the ICFP Papers-track Non-interference Preserving Optimising Compilation
Harshit GargGarg, Harshit Northeastern University - Khoury College of Computer SciencesUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Poorva GargGarg, Poorva University of California, Los AngelesIndia Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Pranav GargGarg, Pranav AWSUnited States UTFix: Change Aware Unit Test Repairing using LLM
Jacques GarrigueGarrigue, Jacques Nagoya UniversityJapan A practical formalization of monadic equational reasoning in dependent-type theory
Antoine GaulinGaulin, Antoine McGill UniversityCanada McTT: A Verified Kernel for a Proof Assistant
François GauthierGauthier, François Oracle LabsAustralia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas GazagnaireGazagnaire, Thomas TaridesFrance Functional Networking for Millions of Docker Desktops (Experience Report)
Yuhao GeGe, Yuhao University of Illinois at Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhaoyi GeGe, Zhaoyi University of WaterlooCanada Zero-Overhead Lexical Effect Handlers
Jasper GeerGeer, Jasper University of British ColumbiaCanada Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Timon GehrGehr, Timon ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Adam T. GellerGeller, Adam T. University of British ColumbiaCanada Type-Preserving Flat Closure Optimization
Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS) Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kimball GermaneGermane, Kimball Brigham Young UniversityUnited States Student Research Competition Chair in Organizing Committee for ICFP 2025 SRC Awards Student Research Competition Chair in Program Committee within the ICFP Student Research Competition-track Session Chair of Algorithms (part of ICFP Papers) Call-Guarded Abstract Definitional Interpreters
Dan GhicaGhica, Dan Huawei Research and University of BirminghamUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mahdi GhorbaniGhorbani, Mahdi University of EdinburghUnited Kingdom Compressed and Parallelized Structured Tensor Algebra
Ryan GibbGibb, Ryan University of Cambridge Functional Networking for Millions of Docker Desktops (Experience Report)
Olek GierczakGierczak, Olek Northeastern University From Linearity to Borrowing
Elizabeth GilbertGilbert, Elizabeth Carnegie Mellon UniversityUnited States Debugging WebAssembly? Put some Whamm on it!
Marco GiuntiGiunti, Marco University of AlgarvePortugal Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Nathan GloverGlover, Nathan Carnegie Mellon University Integrating Resource Analyses via Resource Decomposition
Brighten GodfreyGodfrey, Brighten UIUC and Broadcom SafeTree: Expressive Tree Policies for Microservices
Harrison GoldsteinGoldstein, Harrison University at Buffalo, the State University of New York at BuffaloUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming QED in Context: An Observation Study of Proof Assistant Users
Sergey GoncharovGoncharov, Sergey University of BirminghamUnited Kingdom Bialgebraic Reasoning on Stateful Languages Big Steps in Higher-Order Mathematical Operational Semantics
Léon GondelmanGondelman, Léon Aalborg UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Yeyun GongGong, Yeyun Microsoft Research AutoVerus: Automated Proof Generation for Rust Code
Noah D. GoodmanGoodman, Noah D. Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Kiran GopinathanGopinathan, Kiran University of Illinois Urbana ChampaignUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Colin GordonGordon, Colin Drexel UniversityUnited States Modal Abstractions for Virtualizing Memory Addresses
Roberta GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy Revealing Sources of (Memory) Errors via Backward Analysis
Chester GouldGould, Chester University of British Columbia Type-Preserving Flat Closure Optimization
Hemant GouniGouni, Hemant Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference
John GouwarGouwar, John Northeastern UniversityUnited States Scaling Optimization Over Uncertainty via Compilation
Marcos GranduryGrandury, Marcos IMDEA Software Institute; Universidad Politécnica de MadridSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Zachary GrannanGrannan, Zachary University of British ColumbiaCanada Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Daniel GratzerGratzer, Daniel Aarhus UniversityDenmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
Eva GraversenGraversen, Eva University of Southern Denmark Committee Member in ICFP Programme Committee within the ICFP Papers-track
James Bryan GravesGraves, James Bryan Indiana University A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Gavin GrayGray, Gavin Brown UniversityUnited States A guided tour through Oxidized OCaml
Neville GrechGrech, Neville Dedaub LimitedMalta Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben GreenmanGreenman, Ben University of Utah, USA Workshops Co-Chair in Organizing Committee for ICFP 2025
Ben GreenmanGreenman, Ben University of UtahUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben GreenmanGreenman, Ben University of Utah, USA Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Simon Oddershede GregersenGregersen, Simon Oddershede New York UniversityUnited States Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Karuna GrewalGrewal, Karuna Cornell University SafeTree: Expressive Tree Policies for Microservices
Tobias GrosserGrosser, Tobias University of CambridgeUnited Kingdom Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting Compressed and Parallelized Structured Tensor Algebra
Alexander GryzlovGryzlov, Alexander IMDEA Software InstituteSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Dawu GuGu, Dawu Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yile GuGu, Yile University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Hanqin GuanGuan, Hanqin Peking University Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Kevin GuanGuan, Kevin Cornell UniversityUnited States Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Ege Berkay GulcanGulcan, Ege Berkay Delft University of TechnologyNetherlands Model-guided Fuzzing of Distributed Systems
Ahan GuptaGupta, Ahan University of Illinois at Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Sankha Narayan GuriaGuria, Sankha Narayan University of KansasUnited States Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track OOPSLA Artifact Awards
Claudio GutierrezGutierrez, Claudio DCC, Universidad de Chile & IMFD Flexible and Expressive Typed Path Patterns for GQL
Matthias GüdemannGüdemann, Matthias University of Applied Sciences MunichGermany Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
H Andrew HabibHabib, Andrew ABB Corporate Research, GermanyGermany Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sebastian HackHack, Sebastian Saarland University, Saarland Informatics CampusGermany Non-interference Preserving Optimising Compilation
Finn HackettHackett, Finn University of British ColumbiaCanada TraceLinking Implementations with their Verified Designs
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom The Power of Regular Constraint Propagation
Shashin HalalingaiahHalalingaiah, Shashin UT Austin, IIT MadrasUnited States Probabilistic Inference for Datalog with Correlated Inputs
William HallahanHallahan, William Binghamton Counterexample-Guided Inference of Modular Specifications
Sara S. HamoudaHamouda, Sara S. Canva Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Ameer HamzaHamza, Ameer Florida State UniversityUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Xing HanHan, Xing The Hong Kong University of Science and Technology Agora: Trust Less and Open More in Verification for Confidential Computing
Zhilei HanHan, Zhilei Tsinghua University Structural Abstraction and Refinement for Probabilistic Programs
Dan HaoHao, Dan Peking UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Ben HardekopfHardekopf, Ben University of California at Santa BarbaraUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Zara HassanHassan, Zara Australian National UniversityAustralia Reproducibility Debt in Scientific Software
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Matthias HauswirthHauswirth, Matthias USI LuganoSwitzerland Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chris HawblitzelHawblitzel, Chris Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
Musa HaydarHaydar, Musa University of Michigan Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Dongjie HeHe, Dongjie Chongqing University, ChinaChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Fei HeHe, Fei Tsinghua UniversityChina Structural Abstraction and Refinement for Probabilistic Programs
Jingzhu HeHe, Jingzhu ShanghaiTech UniversityChina Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Pinjia HeHe, Pinjia Chinese University of Hong Kong, ShenzhenChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Siyuan HeHe, Siyuan Purdue University Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Complete the Cycle: Reachability Types with Expressive Cyclic References
Wenyu HeHe, Wenyu Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yituo HeHe, Yituo Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Yumeng HeHe, Yumeng University of Utah Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Andrew HeadHead, Andrew University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Fritz HengleinHenglein, Fritz University of CopenhagenDenmark Committee Member in Distinguished Papers Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Troels HenriksenHenriksen, Troels University of CopenhagenDenmark Correctness Meets Performance: From Agda to Futhark
Martin HenzHenz, Martin National University of SingaporeSingapore Session Chair of Afternoon Paper Session 1 (part of SPLASH -E) SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Felienne HermansHermans, Felienne Vrije Universiteit AmsterdamNetherlands SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Keara HillHill, Keara Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Daniel HillerströmHillerström, Daniel Category Labs and The University of EdinburghUnited Kingdom Modal Effect Types
Ralf HinzeHinze, Ralf RPTU Kaiserslautern-LandauGermany Binary search—think positive
Ralf HinzeHinze, Ralf RPTU Kaiserslautern-Landau Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Session Chair of Concurrency (part of ICFP Papers) Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Martin HirzelHirzel, Martin IBM ResearchUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Son HoHo, Son InriaFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Integrating Resource Analyses via Resource Decomposition
Reid HolmesHolmes, Reid University of British ColumbiaCanada An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Multi-Language Probabilistic Programming Scaling Optimization Over Uncertainty via Compilation
Changwan HongHong, Changwan Massachusetts Institute of Technology Finch: Sparse and Structured Tensor Programming with Control Flow
Weijiang HongHong, Weijiang National University of Defense Technology, Changsha, China Multi-Modal Sketch-based Behavior Tree Synthesis
Manoel Horta RibeiroHorta Ribeiro, Manoel Interactive Theorem Provers for Proof Education
Tony HoskingHosking, Tony Australian National UniversityAustralia Session Chair of Parallelism (part of SPLASH OOPSLA)
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F Committee Member in ICFP Programme Committee within the ICFP Papers-track
Justin HsuHsu, Justin Cornell UniversityUnited States SafeTree: Expressive Tree Policies for Microservices A Hoare Logic For Symmetry Properties
Guangyu HuHu, Guangyu HKUST (The Hong Kong University of Science and Technology) Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jason Z. S. HuHu, Jason Z. S. AmazonUnited States Normalization by Evaluation for Non-cumulativity McTT: A Verified Kernel for a Proof Assistant
Jingmei HuHu, Jingmei Amazon Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yikun HuHu, Yikun Shanghai Jiao Tong UniversityChina Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Effectful Lenses: There and Back with Different Monads Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jeff HuangHuang, Jeff Texas A&M UniversityUnited States DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Lei HuangHuang, Lei ShanghaiTech University Verification of Bit-Flip Attacks against Quantized Neural Networks
Tianshu HuangHuang, Tianshu Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Xuejing HuangHuang, Xuejing IRIFFrance Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging Liberating Merges via Apartness and Guarded Subtyping
Jan HueckelheimHueckelheim, Jan Argonne National Laboratory Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Chris HughesHughes, Chris Independent Researcher Certified Decision Procedures for Width-Independent Bitvector Predicates
Jacob HughesHughes, Jacob King's College LondonUnited Kingdom Garbage Collection for Rust: The Finalizer Frontier
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Nathan HurtigHurtig, Nathan University of WashingtonUnited States Polynomial-Time Program Equivalence for Machine Knitting
Doha HwangHwang, Doha Samsung PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
I Ruxandra IcleanuIcleanu, Ruxandra University of Edinburgh SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Yuka IkarashiIkarashi, Yuka Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Kazuki IkemoriIkemori, Kazuki Tokyo Institute of Technology Continuations for All: Language Design Considerations for Accessible Continuations
Lef IoannidisIoannidis, Lef University of PennsylvaniaUnited States Structural temporal logic for mechanized program verification
Anastasia IsychevIsychev, Anastasia TU WienAustria Cost of Soundness in Mixed-Precision Tuning
J Jules JacobsJacobs, Jules Jane StreetUnited States Web Chair in Organizing Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Koen JacobsJacobs, Koen InriaFrance Robust Dynamic Embedding for Gradual Typing
Seyed Mohammad Reza JafariJafari, Seyed Mohammad Reza Iowa State University Embedding Quantum Program Verification into Dafny
Joxan JaffarJaffar, Joxan National University of SingaporeSingapore Incremental and Unbounded Loop Analysis
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Devansh JainJain, Devansh University of Illinois at Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Vincent James BeardsleyJames Beardsley, Vincent Carapace: Static–Dynamic Information Flow Control in Rust
Dustin JamnerJamner, Dustin MIT CSAIL, USA Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dustin JamnerJamner, Dustin MIT CSAIL Pyrosome: Verified Compilation for Modular Metatheory
Junyoung JangJang, Junyoung McGill UniversityCanada McTT: A Verified Kernel for a Proof Assistant
Patrik JanssonJansson, Patrik Chalmers University of Technology and University of GothenbrugSweden Domain-specific tensor languages
Nikhil JayakumarJayakumar, Nikhil University of Texas at Austin GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Minseok JeonJeon, Minseok DGISTSouth Korea Committee Member in ICFP Programme Committee within the ICFP Papers-track PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Mingyeong JeongJeong, Mingyeong Chungnam National University Type Checking for Python Using Intersection Types
Artur JezJez, Artur University of Wroclaw The Power of Regular Constraint Propagation
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Counterexample-Guided Inference of Modular Specifications
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Ruyi JiJi, Ruyi Peking UniversityChina Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Yuchen JiJi, Yuchen ShanghaiTech University Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Limin JiaJia, Limin Carnegie Mellon University Session Chair of Verification 1 (part of SPLASH OOPSLA) Session Chair of Calculus (part of SPLASH OOPSLA)
Limin JiaJia, Limin Carnegie Mellon UniversityUnited States Quantified Underapproximation via Labeled Bunches
Limin JiaJia, Limin Carnegie Mellon University Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Songlin JiaJia, Songlin Purdue University, USAUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory Complete the Cycle: Reachability Types with Expressive Cyclic References
Jiajun JiangJiang, Jiajun Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Nan JiangJiang, Nan Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi JiangJiang, Shengyi The University of Hong KongChina Normalization by Evaluation for Non-cumulativity
Yuchen JiangJiang, Yuchen University of MichiganUnited States Notions of Stack-manipulating Computation and Relative Monads
Mingyu JoJo, Mingyu Korea University Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Sarah JohnsonJohnson, Sarah Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Max JungJung, Max University of Waterloo Zero-Overhead Lexical Effect Handlers
Ralf JungJung, Ralf ETH ZurichSwitzerland Committee Member in ICFP Programme Committee within the ICFP Papers-track
Sebastian JungesJunges, Sebastian Radboud University A Unifying Approach to Product Constructions for Quantitative Temporal Inference
K Anan KabahaKabaha, Anan Technion, Israel Institute of TechnologyIsrael Quantization with Guaranteed Floating-Point Neural Network Classifications Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification
Rohan KadekodiKadekodi, Rohan University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Gowtham KakiKaki, Gowtham University of Colorado at BoulderUnited States Bolt-On Strong Consistency: Specification, Implementation, and Verification
Konstantinos KallasKallas, Konstantinos University of California, Los AngelesUnited States Opportunistically Parallel Lambda Calculus
Shoaib KamilKamil, Shoaib Adobe Research Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Frex: Dependently Typed Algebraic Simplification Committee Member in ICFP Programme Committee within the ICFP Papers-track
Gabriel KammerKammer, Gabriel MIT Pyrosome: Verified Compilation for Modular Metatheory
Byeongjee KangKang, Byeongjee Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Eunsuk KangKang, Eunsuk Carnegie Mellon UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jeehoon KangKang, Jeehoon FuriosaAISouth Korea Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness Revamping Verilog Semantics for Foundational Verification
Yiping KangKang, Yiping University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Venkata Naga Sai Rohit KantetiKanteti, Venkata Naga Sai Rohit Indian Institute of Technology MadrasIndia Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Ambrus KaposiKaposi, Ambrus ELTE Eötvös Loránd University, Budapest, HungaryHungary Session Chair of Dependent Types (part of ICFP Papers) Type Theory in Type Theory using a Strictified Syntax
Savini KashmiraKashmira, Savini University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baris KasikciKasikci, Baris University of Michigan, USA Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Ryan KavanaghKavanagh, Ryan Université du Québec à MontréalCanada Committee Member in Program Committee within the ICFP Student Research Competition-track Fusing Session-Typed Concurrent Programming into Functional Programming
Alex KavvosKavvos, Alex University of BristolUnited Kingdom Session Chair of Denotational Semantics (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track Adequacy for Algebraic Effects Revisited Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Alex KeizerKeizer, Alex University of Cambridge Interactive Bit Vector Reasoning using Verified Bitblasting
Martin KelloggKellogg, Martin New Jersey Institute of TechnologyUnited States Sponsorship Co-Chair in Organizing Committee for ICFP 2025
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Harun KhanKhan, Harun Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Kaustubh KhulbeKhulbe, Kaustubh University of Illinois at Urbana-Champaign End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Sandra KieferKiefer, Sandra University of Oxford Detecting and explaining (in-)equivalence of context-free grammars
Donguk KimKim, Donguk South Korea PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Hanjun KimKim, Hanjun Yonsei University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hannuri KimKim, Hannuri Chungnam National University Toward Automated Verification of Static Analysis Results of Android Applications
Jaewoo KimKim, Jaewoo KAISTSouth Korea Revamping Verilog Semantics for Foundational Verification
Jieung KimKim, Jieung Yonsei UniversitySouth Korea Session Chair of Verification 4 (part of SPLASH OOPSLA)
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison; Seoul National UniversityUnited States Semantics of Sets of Programs
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Software Model Checking via Summary-Guided Search
Elad KinsbrunerKinsbruner, Elad TechnionIsrael Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Marisa KirisameKirisame, Marisa University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Fredrik KjolstadKjolstad, Fredrik Stanford UniversityUnited States REPTILE: Performant Tiling of Recurrences
Mark KleinKlein, Mark Carnegie Mellon University Quantified Underapproximation via Labeled Bunches
Vasileios KlimisKlimis, Vasileios Queen Mary University of London Shaking Up Quantum Simulators with Fuzzing and Rigour
Mark KochKoch, Mark Quantinuum Fulls Seldom Differ
John C. KolesarKolesar, John C. Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Proof-Carrying Neuro-Symbolic Code
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Type Universes as Kripke Worlds Type-Preserving Flat Closure Optimization
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Abstract Interpretation of Temporal Safety Effects of Higher Order Programs Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Nikita KovalKoval, Nikita JetBrainsNetherlands Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Concurrent Algorithms under the hood of Kotlin Coroutines Testing concurrent code on JVM with Lincheck
András KovácsKovács, András University of Gothenburg and Chalmers University of Technology Committee Member in ICFP Programme Committee within the ICFP Papers-track
Laura KovácsKovács, Laura TU WienAustria Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya Harvard UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
V Krishna NandivadaKrishna Nandivada, V IIT Madras Session Chair of Analysis 2 (part of SPLASH OOPSLA) IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shriram KrishnamurthiKrishnamurthi, Shriram Brown UniversityUnited States Session Chair of Saturday SPLASH Keynote (part of SPLASH Keynotes) RC Chair Report OOPSLA Awards Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track A guided tour through Oxidized OCaml Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Paul KrogmeierKrogmeier, Paul University of Illinois at Urbana-ChampaignUnited States Synthesizing DSLs for Few-Shot Learning
Sachit KuharKuhar, Sachit Amazon Web Services UTFix: Change Aware Unit Test Repairing using LLM
Iona KuhnKuhn, Iona Saarland UniversityGermany Almost Fair Simulations
Burcu Kulahcioglu OzkanKulahcioglu Ozkan, Burcu Delft University of TechnologyNetherlands Model-guided Fuzzing of Distributed Systems
Kouta KumamotoKumamoto, Kouta An Interactive Learning Environment for Program Design
Lindsey KuperKuper, Lindsey University of California, Santa CruzUnited States CRDT Emulation, Simulation, and Representation Independence Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ivan KurajKuraj, Ivan Massachusetts Institute of Technology Peepco: Batch-Based Consistency Optimization
Ismail KuruKuru, Ismail Drexel UniversityUnited States Modal Abstractions for Virtualizing Memory Addresses
Christian KästnerKästner, Christian Carnegie Mellon University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
L Ambroise LafontLafont, Ambroise Inria, France 2-Functoriality of Initial Semantics, and Applications
Patrick LaFontaineLaFontaine, Patrick Purdue UniversityUnited States We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Ignacio LagunaLaguna, Ignacio Lawrence Livermore National LaboratoryUnited States Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
Sumit LahiriLahiri, Sumit Indian Institute of Technology KanpurIndia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cheuk Tung LAILAI, Cheuk Tung VX Research LimitedUnited Kingdom Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Jianxin LaiLai, Jianxin Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Akash LalLal, Akash Microsoft ResearchIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Kait LamLam, Kait Defence Science and Technology Group / School of EECS, University of Queensland Translation Validation for LLVM's AArch64 Backend
Ada LambaLamba, Ada Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Thomas LamiauxLamiaux, Thomas University of Paris-Saclay, Ens Paris-Saclay 2-Functoriality of Initial Semantics, and Applications
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Compositional Quantum Control Flow with Efficient Compilation in Qunity
Jens Kanstrup LarsenLarsen, Jens Kanstrup DTUDenmark Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jacob LaurelLaurel, Jacob Georgia Institute of TechnologyUnited States Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Jonathan LaurentLaurent, Jonathan Carnegie Mellon University / Karlsruhe Institute of Technology Adaptive Shielding via Parametric Safety Proofs
Tom LauwaertsLauwaerts, Tom Universiteit Gent, BelgiumBelgium MIO: Multiverse Debugging in the face of Input/Output
Tony LawLaw, Tony Univ Rennes, Inria, CNRS, IRISA A Mechanized Semantics for Dataflow Circuits
Julia LawallLawall, Julia InriaFrance Automating maintenance of the Linux kernel: a perspective over 20 years
Alan LawrenceLawrence, Alan Quantinuum Fulls Seldom Differ
Isabella LaybournLaybourn, Isabella Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Doug LeaLea, Doug State University of New York (SUNY) OswegoUnited States Soundness of Predictive Concurrency Analyses
Ashley LeeLee, Ashley University of California, Santa Cruz SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Dongjae LeeLee, Dongjae Massachusetts Institute of Technology Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Edward LeeLee, Edward University of Waterloo; University of Toronto ScarboroughCanada Qualified Types with Boolean Algebras
Janggun LeeLee, Janggun KAIST Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Jay LeeLee, Jay Seoul National UniversitySouth Korea React-tRace: A Semantics for Understanding React Hooks
Juneyoung LeeLee, Juneyoung AWS Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Keonho LeeLee, Keonho University of California, Irvine Towards Verifying Crash Consistency
Leo Seojun LeeLee, Leo Seojun University of OxfordUnited Kingdom Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Shaun Christopher LeeLee, Shaun Christopher University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Sungho LeeLee, Sungho Chungnam National University, KoreaSouth Korea Simplifying Lifter-generated Emulation Style LLVM IR for Analysis Suitability Type Checking for Python Using Intersection Types Toward Automated Verification of Static Analysis Results of Android Applications
Woosuk LeeLee, Woosuk Hanyang UniversitySouth Korea Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunjeong LeeLee, Yunjeong National University of SingaporeSingapore Student Volunteer Co-Chair in Organizing Committee for ICFP 2025
Zheng Han LeeLee, Zheng Han National University of Singapore, Singapore Efficient Decrease-And-Conquer Linearizability Monitoring
Owolabi LegunsenLegunsen, Owolabi Cornell UniversityUnited States Session Chair of Testing 2 (part of SPLASH OOPSLA) Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Daan LeijenLeijen, Daan Microsoft ResearchUnited States First-Order Laziness
Caroline LemieuxLemieux, Caroline University of British ColumbiaCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Damitha LenadoraLenadora, Damitha University of Illinois at Urbana-Champaign GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Connor LenihanLenihan, Connor King's College London Shaking Up Quantum Simulators with Fuzzing and Rigour AccelerQ: Accelerating Quantum Eigensolvers With Machine Learning on Quantum Simulators
John LeoLeo, John Halfaya ResearchUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Mohsen LesaniLesani, Mohsen University of California at Santa Cruz Hambazi: Spatial Coordination Synthesis for Augmented Reality
Martin LesterLester, Martin University of ReadingUnited Kingdom Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Kyla H. LevinLevin, Kyla H. University of Massachusetts Amherst, USAUnited States RestPi: Path-Sensitive Type Inference for REST APIs
Reese LevineLevine, Reese SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Nicholas V. LewchenkoLewchenko, Nicholas V. University of Colorado BoulderUnited States Bolt-On Strong Consistency: Specification, Implementation, and Verification
Ondřej LhotákLhoták, Ondřej University of WaterlooCanada A simple blame calculus for explicit nulls Flix: A Design for Language-Integrated Datalog Qualified Types with Boolean Algebras
Ao LiLi, Ao Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Baichuan LiLi, Baichuan University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Baixuan LiLi, Baixuan School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University ABC: Towards a Universal Code Styler through Model Merging
Chenxi LiLi, Chenxi Nanjing University, China Two Approaches to Fast Bytecode Frontend for Static Analysis
Chenxing LiLi, Chenxing Shanghai Tree-Graph Blockchain Research InstituteChina HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Ding LiLi, Ding Peking UniversityChina Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Elaine LiLi, Elaine NYUUnited States Characterizing Implementability of Global Protocols with Infinite States and Data
Guanyan LiLi, Guanyan University of Oxford Structural Abstraction and Refinement for Probabilistic Programs
Haofeng LiLi, Haofeng SKLP, Institute of Computing Technology, CASChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Haoran LiLi, Haoran Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Jianlin LiLi, Jianlin University of WaterlooCanada Compiling with Generating Functions
John LiLi, John Northeastern UniversityUnited States Multi-Language Probabilistic Programming From Linearity to Borrowing
Juanen LiLi, Juanen Beijing Normal University Structural Abstraction and Refinement for Probabilistic Programs
Kwing Hei LiLi, Kwing Hei Aarhus UniversityDenmark Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Lian LiLi, Lian Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Liyi LiLi, Liyi Iowa State UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware Embedding Quantum Program Verification into Dafny
Long LiLi, Long Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Mingyi LiLi, Mingyi Institute of Computing Technology, CASChina Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peilun LiLi, Peilun Shanghai Tree-Graph Blockchain Research Institute HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Shangyu LiLi, Shangyu The Hong Kong University of Science and Technology A Sound Static Analysis Approach to I/O API Migration
Shaohua LiLi, Shaohua The Chinese University of Hong KongHong Kong SAR China An Empirical Study of Bugs in the rustc Compiler Interleaving Large Language Models for Compiler Testing
Tianchi LiLi, Tianchi Peking University, ChinaChina Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
Wu Angela LiLi, Wu Angela Rice University Efficient Algorithms for the Uniform Tokenization Problem
Xuandong LiLi, Xuandong Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Xuheng LiLi, Xuheng Columbia University AutoVerus: Automated Proof Generation for Rust Code
Xuyang LiLi, Xuyang Purdue University Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Yi LiLi, Yi Nanyang Technological UniversitySingapore TailTracer: Continuous Tail Tracing for Production Use
Yihe LiLi, Yihe National University of Singapore Large Language Model powered Symbolic Execution
Yue LiLi, Yue Nanjing UniversityChina Two Approaches to Fast Bytecode Frontend for Static Analysis
Zhong LiLi, Zhong Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Qihao LianLian, Qihao Peking UniversityChina Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Peng LiangLiang, Peng Wuhan University, ChinaChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Nathan LiittschwagerLiittschwager, Nathan University of California, Santa Cruz CRDT Emulation, Simulation, and Representation Independence
Anthony Widjaja LinLin, Anthony Widjaja RPTU Kaiserslautern-Landau and Max-Planck Institute for Software Systems The Power of Regular Constraint Propagation
Haoran LinLin, Haoran Nanjing University, China Two Approaches to Fast Bytecode Frontend for Static Analysis
Jenny Han LinLin, Jenny Han University of UtahUnited States Polynomial-Time Program Equivalence for Machine Knitting
Youfang LinLin, Youfang Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom ICFP'23 Program Chair in Steering Committee for ICFP 2025 First-Order Laziness Modal Effect Types
Benjamin LionLion, Benjamin INRIA Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Kyle LittleLittle, Kyle University of Utah SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Cyrus LiuLiu, Cyrus Samsung SemiconductorUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Hanzhi LiuLiu, Hanzhi University of California, Santa Barbara & Riema LabsUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Junrui LiuLiu, Junrui University of California, Santa BarbaraUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Kui LiuLiu, Kui HuaweiChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Lang LiuLiu, Lang Illinois Institute of Technology Quantified Underapproximation via Labeled Bunches
Shuyang LiuLiu, Shuyang Soundness of Predictive Concurrency Analyses
Tianyi LiuLiu, Tianyi Nanjing UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Xinxin LiuLiu, Xinxin Institute of software, Chinese academy of sciences HpC: A Calculus for Hybrid and Mobile Systems
Yan LiuLiu, Yan Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Zixi LiuLiu, Zixi Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Francesco LogozzoLogozzo, Francesco MetaUnited States Revealing Sources of (Memory) Errors via Backward Analysis
Debasmita LoharLohar, Debasmita Karlsruhe Institute of TechnologyGermany Cost of Soundness in Mixed-Precision Tuning
Tommie LombartsLombarts, Tommie Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Fan LongLong, Fan University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Nuno P. LopesLopes, Nuno P. INESC-ID; Instituto Superior Técnico - University of LisbonPortugal Translation Validation for LLVM's AArch64 Backend
Jacob R. LorchLorch, Jacob R. Microsoft Research, n.n. AutoVerus: Automated Proof Generation for Rust Code
Anton LorenzenLorenzen, Anton University of EdinburghUnited Kingdom First-Order Laziness Modal Effect Types
Yiling LouLou, Yiling University of Illinois at Urbana-ChampaignUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Jiayi LuLu, Jiayi Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Jie LuLu, Jie SKLP, Institute of Computing Technology, CAS, China Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Longlong LuLu, Longlong State Key Laboratory for Novel Software Technology, Nanjing University, China Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Shan LuLu, Shan Microsoft; University of ChicagoUnited States AutoVerus: Automated Proof Generation for Rust Code
Shuai LuLu, Shuai Microsoft ResearchChina AutoVerus: Automated Proof Generation for Rust Code
Sirui LuLu, Sirui OpenAIUnited States HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Yifei LuLu, Yifei State Key Laboratory for Novel Software Technology, Nanjing University, China Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Yunping LuLu, Yunping Fudan University JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Mingyuan LuoLuo, Mingyuan Fudan University ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Ning LuoLuo, Ning UIUCUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Matthew LutzeLutze, Matthew Aarhus University The Simple Essence of Monomorphization
Júnior LöffLöff, Júnior Università della Svizzera italiana HeapBuffers: Why not just using a binary serialization format for your managed memory?
Andreas LööwLööw, Andreas Imperial College LondonUnited Kingdom The Simulation Semantics of Synthesisable Verilog Compositional Symbolic Execution for the Next 700 Memory Models
M Chenyang MaMa, Chenyang Nanjing University of Science and Technology DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Cong MaMa, Cong University of WaterlooCanada Zero-Overhead Lexical Effect Handlers
Hui MaMa, Hui Institute of Computing Technology, Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Xiaofei MaMa, Xiaofei AWS AI Labs UTFix: Change Aware Unit Test Repairing using LLM
Xiaotian MaMa, Xiaotian Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Zhongkui MaMa, Zhongkui The University of QueenslandAustralia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Convex Hull Approximation for Activation Functions
Aravind MachiryMachiry, Aravind Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Julian MackayMackay, Julian Kry10 Ltd Reasoning about External Calls
Stefan MadaMada, Stefan University of Utah Translation Validation for LLVM's AArch64 Backend
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom Committee Member in Program Committee within the ICFP Student Research Competition-track Functional Networking for Millions of Docker Desktops (Experience Report) A guided tour through Oxidized OCaml
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States FO-Complete Program Verification for Heap Logics Synthesizing DSLs for Few-Shot Learning
Jean-Marie MadiotMadiot, Jean-Marie InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Magnus MadsenMadsen, Magnus Aarhus UniversityDenmark Flix: A Design for Language-Integrated Datalog Qualified Types with Boolean Algebras Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Enrico MagnagoMagnago, Enrico Amazon Web Services Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Romina MahinpeiMahinpei, Romina Princeton University Interactive Theorem Provers for Proof Education
Daryl MaierMaier, Daryl IBM CanadaCanada CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Kenji MaillardMaillard, Kenji Inria – LS2N, Université de NantesFrance Incremental Certified Programming
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Model-guided Fuzzing of Distributed Systems
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Efficient Algorithms for the Uniform Tokenization Problem
Wensen MaoMao, Wensen Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Michaël MarcozziMarcozzi, Michaël Université Paris-Saclay, CEA, ListFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dylan MarinhoMarinho, Dylan Sorbonne Université, CNRS UMR 7606, LIP6, Paris, FranceFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oliver MarkgrafMarkgraf, Oliver RPTU Kaiserslautern-Landau The Power of Regular Constraint Propagation
Petros MarkopoulosMarkopoulos, Petros Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Stefan MarrMarr, Stefan Johannes Kepler University LinzAustria Session Chair of Debugging and Validation (part of SPLASH OOPSLA) Session Chair of Runtime (part of SPLASH OOPSLA) Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jason MarsMars, Jason University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Brianna MarshallMarshall, Brianna Northeastern UniversityUnited States From Linearity to Borrowing
Chris MartensMartens, Chris Northeastern UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ruben MartinsMartins, Ruben Carnegie Mellon UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guido MartínezMartínez, Guido Microsoft ResearchUnited States SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Kristóf MarussyMarussy, Kristóf Budapest University of Technology and EconomicsHungary Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hidehiko MasuharaMasuhara, Hidehiko Institute of Science TokyoJapan Session Chair of Compilation 3 (part of SPLASH OOPSLA) Session Chair of Compilation 1 (part of SPLASH OOPSLA) Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track An Interactive Learning Environment for Program Design Daisy: An Exercise Environment for Learning Information Modeling
Sebastian Mateos NicolajsenMateos Nicolajsen, Sebastian IT University of CopenhagenDenmark Committee Member in Program Commitee within the SPLASH -E-track
Umang MathurMathur, Umang National University of SingaporeSingapore Efficient Decrease-And-Conquer Linearizability Monitoring Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Umang MathurMathur, Umang National University of Singapore, SingaporeSingapore View Types in Rust
Damiano MazzaMazza, Damiano CNRS, LIPN, Université Sorbonne Paris NordFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Conor McBrideMcBride, Conor University of Strathclyde Fulls Seldom Differ
James McCannMcCann, James Carnegie Mellon UniversityUnited States Polynomial-Time Program Equivalence for Machine Knitting
Kathryn S McKinleyMcKinley, Kathryn S Google Advancing Performance via a Systematic Application of Research and Industrial Best Practice Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Michael McLoughlinMcLoughlin, Michael Carnegie Mellon UniversityUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Vaibhav MehtaMehta, Vaibhav Cornell UniversityUnited States A Hoare Logic For Symmetry Properties
Antero MejrMejr, Antero Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Olivier MelançonMelançon, Olivier Université de MontréalCanada Float Self-Tagging
Orestis MelkonianMelkonian, Orestis Input Output Global (IOG/IOHK)United Kingdom Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Stephen MellMell, Stephen University of Pennsylvania Opportunistically Parallel Lambda Calculus
Guillaume MelquiondMelquiond, Guillaume Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Charith MendisMendis, Charith University of Illinois at Urbana-ChampaignUnited States Automated Verification of Soundness of DNN Certifiers GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Ruijie MengMeng, Ruijie National University of Singapore, SingaporeSingapore Large Language Model powered Symbolic Execution
Mae MilanoMilano, Mae Princeton UniversityUnited States Session Chair of LGBTQ Lunch (part of ICFP Diversity, Equity, and Inclusion) Interactive Theorem Provers for Proof Education
Stefan MiliusMilius, Stefan Friedrich-Alexander University Erlangen-NürnbergGermany Bialgebraic Reasoning on Stateful Languages
Heather MillerMiller, Heather Carnegie Mellon University and Two Sigma Debugging WebAssembly? Put some Whamm on it!
Todd MillsteinMillstein, Todd University of California at Los AngelesUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming Synthesizing Implication Lemmas for Interactive Theorem Proving
Tijana MinićMinić, Tijana Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Mikhail MintsMints, Mikhail California Institute of TechnologyUnited States Compositional Quantum Control Flow with Efficient Compilation in Qunity
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Ashish MishraMishra, Ashish IIT HyderabadIndia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Md Rakib Hossain MisuMisu, Md Rakib Hossain University of California IrvineUnited States AutoVerus: Automated Proof Generation for Rust Code
Sidi Mohamed BeillahiMohamed Beillahi, Sidi University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Abdalrhman MohamedMohamed, Abdalrhman Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Alexandre MoineMoine, Alexandre New York UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Evgenii MoiseenkoMoiseenko, Evgenii JetBrains Research Testing concurrent code on JVM with Lincheck
Abtin MolaviMolavi, Abtin University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures Compiling Quantum Circuits
Benoît MontaguMontagu, Benoît InriaFrance Artifact Evaluation Co-Chair in Organizing Committee for ICFP 2025 Artifact Evaluation Co-Chair in Artifact Evaluation Committe within the ICFP Artifacts-track
Fabrizio MontesiMontesi, Fabrizio University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Arjan J. MooijMooij, Arjan J. Zürich University of Applied Sciences Language-Parametric Reference Synthesis
David MoonMoon, David University of MichiganUnited States Syntactic Completions with Material Obligations
Angelica MoreiraMoreira, Angelica Microsoft ResearchCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gabriel A. MorenoMoreno, Gabriel A. Carnegie Mellon University Software Engineering InstituteUnited States Quantified Underapproximation via Labeled Bunches
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Teaching Software Specification (Experience Report)
Shin-Cheng MuMu, Shin-Cheng Academia Sinica, TaiwanTaiwan Bottom-up computation using trees of sublists
Fabian MuehlboeckMuehlboeck, Fabian Australian National UniversityAustralia View Types in Rust
Eric MugnierMugnier, Eric University of California San Diego On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Serkan MuhcuMuhcu, Serkan Technische Universität Berlin Multiple Resumptions and Local Mutable State, Directly
Prasita MukherjeeMukherjee, Prasita Purdue University KestRel: Relational Verification Using E-Graphs for Program Alignment
Adithya MuraliMurali, Adithya University of Illinois at Urbana-ChampaignUnited States FO-Complete Program Verification for Heap Logics
Charlie MurphyMurphy, Charlie Amazon Web Services, USAUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Gail MurphyMurphy, Gail University of British ColumbiaCanada An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Andrew MyersMyers, Andrew Cornell University SIGPLAN Chair in Steering Committee for ICFP 2025
Anders MøllerMøller, Anders Aarhus UniversityDenmark SIGPLAN Vice Chair in Steering Committee for ICFP 2025
Marius MüllerMüller, Marius University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Peter MüllerMüller, Peter ETH ZurichSwitzerland Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees Modular Reasoning about Global Variables and Their Initialization A Refinement Methodology for Distributed Programs in Rust
N Ritam NagNag, Ritam MIT Pyrosome: Verified Compilation for Modular Metatheory
Kartik NagarNagar, Kartik IIT MadrasIndia Automatically Verifying Replication-aware Linearizability Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Srinidhi NagendraNagendra, Srinidhi IRIF, Chennai Mathematical InstituteFrance Model-guided Fuzzing of Distributed Systems
Shaan NagyNagy, Shaan University of Wisconsin-Madison Semantics of Sets of Programs
Tomoki NakamaruNakamaru, Tomoki The University of TokyoJapan Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Chandrakana NandiNandi, Chandrakana CertoraUnited States Workshops Co-Chair in Organizing Committee for ICFP 2025 Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Daniele Nantes-SobrinhoNantes-Sobrinho, Daniele Imperial College LondonUnited Kingdom Compositional Symbolic Execution for the Next 700 Memory Models
Nuntipat NarkthongNarkthong, Nuntipat Northeastern UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jorge A. NavasNavas, Jorge A. CertoraUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Ian NealNeal, Ian University of Michigan and Veridise Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Luca NegriniNegrini, Luca Ca’ Foscari University of VeniceItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Vladyslav NekriachNekriach, Vladyslav University Of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Tim NelsonNelson, Tim Brown UniversityUnited States Committee Member in Program Commitee within the SPLASH -E-track
Max S. NewNew, Max S. University of MichiganUnited States Notions of Stack-manipulating Computation and Relative Monads
Hoan NguyenNguyen, Hoan Amazon Web Services Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yunbo NiNi, Yunbo The Chinese University of Hong KongHong Kong SAR China An Empirical Study of Bugs in the rustc Compiler Interleaving Large Language Models for Compiler Testing
Mihai NicolaNicola, Mihai Stevens Institute of Technology Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Yue NiuNiu, Yue National Institute of Informatics Integrating Resource Analyses via Resource Decomposition
James NobleNoble, James Independent. Wellington, NZNew Zealand Reasoning about External Calls Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michael NorrishNorrish, Michael Australian National UniversityAustralia Reproducibility Debt in Scientific Software
Aman NougrahiyaNougrahiya, Aman IIT MadrasIndia IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Jose Nuno OliveiraNuno Oliveira, Jose University of Minho; INESC TECPortugal How much is in a square? Calculating functional programs with squares
O Liam O'ConnorO'Connor, Liam Australian National UniversityAustralia Programming Contest Organiser in Organizing Committee for ICFP 2025 ICFP Contest Report Committee Member in ICFP Programme Committee within the ICFP Papers-track
Lina OchoaOchoa, Lina Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Martin OderskyOdersky, Martin EPFLSwitzerland What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Hakjoo OhOh, Hakjoo Korea UniversitySouth Korea Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Semantics (part of SPLASH OOPSLA) Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina Normalization by Evaluation for Non-cumulativity Session Chair of Languages (part of SPLASH OOPSLA) Flexible and Expressive Typed Path Patterns for GQL (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging Liberating Merges via Apartness and Guarded Subtyping
Luca OlivieriOlivieri, Luca Ca’ Foscari University of VeniceItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Cyrus OmarOmar, Cyrus University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Syntactic Completions with Material Obligations
Dominic OrchardOrchard, Dominic University of Cambridge; University of KentUnited Kingdom Session Chair of Types and Specifications (part of ICFP Papers)
Klaus OstermannOstermann, Klaus University of TübingenGermany Committee Member in ICFP Programme Committee within the ICFP Papers-track Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Rodrigo OtoniOtoni, Rodrigo USI LuganoSwitzerland A Language for Quantifying Quantum Network Behavior
P Rohan PadhyePadhye, Rohan Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Oded PadonPadon, Oded Weizmann Institute of ScienceIsrael Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sreepathi PaiPai, Sreepathi University of RochesterUnited States Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
Sasha PakPak, Sasha Australian National UniversityAustralia Verifying Extract Method Refactoring in Rust View Types in Rust
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Session Chair of Quantum (part of SPLASH OOPSLA) Soundness of Predictive Concurrency Analyses
Minxue PanPan, Minxue Nanjing UniversityChina Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Naomi PandaPanda, Naomi Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Akash PardeshiPardeshi, Akash University of Illinois at Urbana-ChampaignUnited States End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Pavel ParizekParizek, Pavel Charles University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jihee ParkPark, Jihee KAISTSouth Korea Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Jihyeok ParkPark, Jihyeok Korea UniversitySouth Korea Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Kanghee ParkPark, Kanghee University of Wisconsin-MadisonUnited States LOUD: Synthesizing Strongest and Weakest Specifications
Seung Hoon ParkPark, Seung Hoon Imperial College London Compositional Symbolic Execution for the Next 700 Memory Models
Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Lionel ParreauxParreaux, Lionel HKUST (The Hong Kong University of Science and Technology)Hong Kong SAR China Artifact Evaluation Co-Chair in Organizing Committee for ICFP 2025 Artifact Evaluation Co-Chair in Artifact Evaluation Committe within the ICFP Artifacts-track Session Chair of Theory (part of SPLASH OOPSLA) Session Chair of Type 1 (part of SPLASH OOPSLA) A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation With Constraint-Based Subtype Inference Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Pouya PartowPartow, Pouya Birmingham University Big Steps in Higher-Order Mathematical Operational Semantics
Radha PatelPatel, Radha MIT CSAIL Finch: Sparse and Structured Tensor Programming with Control Flow
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited States Committee Member in Program Committee within the ICFP Student Research Competition-track Teaching Software Specification (Experience Report) SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Luke PearsonPearson, Luke Polychain Capital Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Anurudh PeduriPeduri, Anurudh Ruhr University Bochum QbC: Quantum Correctness by Construction
Yu PeiPei, Yu Hong Kong Polytechnic UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Daniel A. A. PelsmaekerPelsmaeker, Daniel A. A. Delft University of Technology, NetherlandsNetherlands Language-Parametric Reference Synthesis
Mai Jacob PengPeng, Mai Jacob McGill UniversityCanada Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Wei PengPeng, Wei Fudan University JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Xuanyu PengPeng, Xuanyu University of California, San DiegoUnited States LOUD: Synthesizing Strongest and Weakest Specifications
Yiteng PengPeng, Yiteng Hong Kong University of Science and TechnologyChina Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
João PereiraPereira, João ETH Zurich Modular Reasoning about Global Variables and Their Initialization A Refinement Methodology for Distributed Programs in Rust
Mário PereiraPereira, Mário NOVA LINCS & DI -- Nova School of Science and TechnologyPortugal Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Daniel PerelmanPerelman, Daniel MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Basile PesinPesin, Basile Ecole Nationale de l'Aviation Civile (ENAC) Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Edward PetersPeters, Edward Pushing the Information-Theoretic Limits of Random Access Lists
Anja Petković KomelPetković Komel, Anja Argot Collective Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Daniela PetrisanPetrisan, Daniela IRIF, Université Paris DiderotFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Loïc PeyrotPeyrot, Loïc IMDEA Software Institute Polymorphic Records for Dynamic Languages
Simon Peyton JonesPeyton Jones, Simon Epic Games United Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Structural Information Flow: A Fresh Look at Types for Non-Interference
Long PhamPham, Long Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition
Nguyen PhamPham, Nguyen EPFL, LAMPSwitzerland What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Phitchaya Mangpo PhothilimthanaPhothilimthana, Phitchaya Mangpo OpenAI Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
David PichardiePichardie, David MetaFrance Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Lauren PickPick, Lauren The Chinese University of Hong Kong Checking Observational Correctness of Database Systems
Brigitte PientkaPientka, Brigitte McGill UniversityCanada ICFP '24 Program Chair in Steering Committee for ICFP 2025 McTT: A Verified Kernel for a Proof Assistant Fusing Session-Typed Concurrent Programming into Functional Programming
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming QED in Context: An Observation Study of Proof Assistant Users Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Frank PiessensPiessens, Frank KU LeuvenBelgium Software Stacks for Confidential Computing Hardware
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Counterexample-Guided Inference of Modular Specifications Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
André PlatzerPlatzer, André Karlsruhe Institute of Technology (KIT)Germany Adaptive Shielding via Parametric Safety Proofs
Dan PlyukhinPlyukhin, Dan University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Gabriel PoesiaPoesia, Gabriel Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Peepco: Batch-Based Consistency Optimization Laurel: Unblocking Automated Verification with Large Language Models
Thomas J. PorterPorter, Thomas J. University of MichiganUnited States Incremental Bidirectional Typing via Order Maintenance Syntactic Completions with Material Obligations
Alex PotaninPotanin, Alex Australian National UniversityAustralia SIGPLAN Awards SPLASH Awards Embedding Quantum Program Verification into Dafny SPLASH Organisers Discussion and AMA Verifying Extract Method Refactoring in Rust Reproducibility Debt in Scientific Software View Types in Rust
François PottierPottier, François InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Pontakorn PrasertsukPrasertsuk, Pontakorn Singapore Evolving How We Teach Memory Models
Thomas S. PricePrice, Thomas S. Carnegie Mellon UniversityUnited States Polynomial-Time Program Equivalence for Machine Knitting
Aleksandar ProkopecProkopec, Aleksandar Oracle LabsSwitzerland Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Loïc PujetPujet, Loïc Stockholm University Type Theory in Type Theory using a Strictified Syntax
Q Yong Qi FooQi Foo, Yong National University of SingaporeSingapore Pushing the Information-Theoretic Limits of Random Access Lists
Xueying QinQin, Xueying University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Weihao QuQu, Weihao University at Buffalo, SUNY Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Andrew QuinnQuinn, Andrew University of California at Santa CruzUnited States Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Benjamin QuiringQuiring, Benjamin University of Maryland at College ParkUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimi RacordonRacordon, Dimi EPFLSwitzerland Existentialize your Generics
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited States A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Shanto RahmanRahman, Shanto The University of Texas at AustinUnited States UTFix: Change Aware Unit Test Repairing using LLM Understanding and Improving Flaky Test Classification
Sophie RainRain, Sophie Argot Collective Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Gokul RajivRajiv, Gokul National University of Singapore, SingaporeSingapore Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Ramya RamalingamRamalingam, Ramya University of Pennsylvania Active Learning for Neurosymbolic Program Synthesis
Arjun RameshRamesh, Arjun Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Robert RandRand, Robert University of ChicagoUnited States Compositional Quantum Control Flow with Efficient Compilation in Qunity A Language for Quantifying Quantum Network Behavior
Francesca RandoneRandone, Francesca Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Marianna RapoportRapoport, Marianna Amazon Web ServicesCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Joseph RaskindRaskind, Joseph SUNY Binghamton Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia Automatically Verifying Replication-aware Linearizability
Savitha RaviRavi, Savitha UC San Diego An Empirical Evaluation of Property-Based Testing in Python
Michael RawsonRawson, Michael University of SouthamptonUnited Kingdom Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Baishakhi RayRay, Baishakhi Columbia UniversityUnited States UTFix: Change Aware Unit Test Repairing using LLM
Patrick RedmondRedmond, Patrick University of California, Santa Cruz Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
John RegehrRegehr, John University of UtahUnited States Translation Validation for LLVM's AArch64 Backend
Baber RehmanRehman, Baber University of Hong KongHong Kong SAR China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Hamza RemmalRemmal, Hamza EPFL, LAMPSwitzerland Existentialize your Generics
John ReppyReppy, John University of ChicagoUnited States Session Chair of Clever Compilation (part of ICFP Papers) Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages Committee Member in ICFP Programme Committee within the ICFP Papers-track
Thomas RepsReps, Thomas University of Wisconsin-MadisonUnited States Software Model Checking via Summary-Guided Search (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs Semantics of Sets of Programs Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Mohammad RezaalipourRezaalipour, Mohammad University of PassauGermany Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jaspreet RiarRiar, Jaspreet Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Jay RichardsRichards, Jay University of Kent Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Bryan RichlinskiRichlinski, Bryan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Manuel RiggerRigger, Manuel National University of SingaporeSingapore Flexible and Expressive Typed Path Patterns for GQL Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Talia Lily RingerRinger, Talia Lily University of Illinois Urbana-ChampaignUnited States Proof Repair across Quotient Type Equivalences
Exequiel RivasRivas, Exequiel Tallinn University of Technology; Ahrefs SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Cody RiveraRivera, Cody University of Illinois, Urbana-Champaign Checking $\delta$-Satisfiability of Reals with Integrals
Tiark RompfRompf, Tiark Purdue UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory Complete the Cycle: Reachability Types with Expressive Cyclic References
Julian RosemannRosemann, Julian Saarland University, Saarland Informatics CampusGermany Non-interference Preserving Optimising Compilation
Andrea RosàRosà, Andrea USI LuganoSwitzerland Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Jurriaan RotRot, Jurriaan Radboud University Nijmegen A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Anthony RoweRowe, Anthony Carnegie Mellon University Unveiling Heisenbugs with Diversified Execution
Radosław Jan RowickiRowicki, Radosław Jan Technical University of DenmarkDenmark Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Craig RoyRoy, Craig Quantinuum Fulls Seldom Differ
Subhajit RoyRoy, Subhajit IIT KanpurIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Fabian RuchRuch, Fabian UnaffiliatedSweden Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Philipp RuemmerRuemmer, Philipp University of Regensburg and Uppsala UniversityGermany The Power of Regular Constraint Propagation
Neea RuschRusch, Neea Augusta UniversityUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Alejandro RussoRusso, Alejandro Chalmers University of Technology, Sweden / University of Gothenburg, Sweden / DPella AB, SwedenSweden Diversity Co-Chair in Organizing Committee for ICFP 2025 Diversity Co-Chair in Steering Committee for ICFP 2025
Yeonhee RyouRyou, Yeonhee KAISTSouth Korea Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Session Chair of Thursday SPLASH Keynote (part of SPLASH Keynotes) Session Chair of Verification 2 (part of SPLASH OOPSLA) Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation RC Chair Report OOPSLA Awards Co-chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
S William S. MosesS. Moses, William University of Illinois Urbana-ChampaignUnited States Sound and Modular Activity Analysis for Automatic Differentiation in MLIR Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Feras SaadSaad, Feras Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition
Amr SabrySabry, Amr Indiana UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Hannes SaffrichSaffrich, Hannes University of Freiburg Borrowing From Session Types
Sunita SahaSaha, Sunita German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Ayman SaidSaid, Ayman University of Michigan Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Takafumi SaikawaSaikawa, Takafumi Nagoya UniversityJapan A practical formalization of monadic equational reasoning in dependent-type theory
Kazuhiko SakaguchiSakaguchi, Kazuhiko CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668France Committee Member in Program Committee within the ICFP Student Research Competition-track A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
Marie SalomonSalomon, Marie University of British ColumbiaCanada An Exploration of How Generative AI Affects Workflow and Collaboration in a Software Engineering Course
Michael SammlerSammler, Michael Institute of Science and Technology AustriaAustria Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ashley SamuelsonSamuelson, Ashley University of Wisconsin-MadisonUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
David SananSanan, David Singapore Institute of TechnologySingapore A complete formal semantics of eBPF instruction set architecture for Solana
Chuta SanoSano, Chuta McGill UniversityCanada Fusing Session-Typed Concurrent Programming into Functional Programming
André L. SantosSantos, André L. University Institute of Lisbon, Portugal Committee Member in Program Commitee within the SPLASH -E-track
Yasmin Chandini SaritaSarita, Yasmin Chandini UIUC Automated Verification of Soundness of DNN Certifiers
Kartik SathyanarayananSathyanarayanan, Kartik Netflix, Inc. Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Alceste ScalasScalas, Alceste Technical University of DenmarkDenmark Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Ina SchaeferSchaefer, Ina KITGermany QbC: Quantum Correctness by Construction
Daniel SchemmelSchemmel, Daniel Imperial College London P³: Reasoning about Patches via Product Programs
Gabriel SchererScherer, Gabriel Université Paris Cité - Inria - CNRSFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Marko SchmellenkampSchmellenkamp, Marko Ruhr University BochumGermany Detecting and explaining (in-)equivalence of context-free grammars
Bradley SchmerlSchmerl, Bradley School of Computer Science, Carnegie Mellon University ROSpec: A Domain-Specific Language for ROS-based Robot Software
Valentin SchneebergerSchneeberger, Valentin EPFL Logically Qualified Types for Scala
Matthew SchneiderSchneider, Matthew Carnegie Mellon UniversityUnited States Debugging WebAssembly? Put some Whamm on it!
Christophe ScholliersScholliers, Christophe Universiteit Gent, Belgium MIO: Multiverse Debugging in the face of Input/Output
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Effectful Lenses: There and Back with Different Monads
Lutz SchröderSchröder, Lutz Friedrich-Alexander University Erlangen-NürnbergGermany Bialgebraic Reasoning on Stateful Languages
Michael SchröderSchröder, Michael TU WienAustria Static Inference of Regular Grammars for Ad Hoc Parsers
Manuela SchulerSchuler, Manuela German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Adriana SchulzSchulz, Adriana University of WashingtonUnited States Polynomial-Time Program Equivalence for Machine Knitting
Philipp SchusterSchuster, Philipp University of TübingenGermany Multiple Resumptions and Local Mutable State, Directly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Dynamic Wind for Effect Handlers Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation The Simple Essence of Monomorphization
David J. ScottScott, David J. Docker, Inc. Functional Networking for Millions of Docker Desktops (Experience Report)
Remy SeassauSeassau, Remy InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Mazyar SerajSeraj, Mazyar Eindhoven University of TechnologyNetherlands Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises Committee Member in Program Commitee within the SPLASH -E-track
Ilya SergeySergey, Ilya National University of SingaporeSingapore General Chair in Organizing Committee for ICFP 2025 ICFP'25 General Chair in Steering Committee for ICFP 2025 General Chair Report Opening Award Ceremony Session Chair of Monday ICFP Keynote (part of ICFP Keynotes) Inductive Synthesis of Inductive Heap Predicates
Manuel SerranoSerrano, Manuel Inria; Université Côte d’AzurFrance Chair in Distinguished Papers Committee for ICFP 2025 Associate Chair in ICFP Programme Committee within the ICFP Papers-track Session Chair of Memory (part of SPLASH OOPSLA) Float Self-Tagging Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Sanjit A. SeshiaSeshia, Sanjit A. University of California, BerkeleyUnited States Checking Observational Correctness of Database Systems
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Compressed and Parallelized Structured Tensor Algebra
Arindam SharmaSharma, Arindam Imperial College London P³: Reasoning about Patches via Product Programs
Jiasi ShenShen, Jiasi The Hong Kong University of Science and Technology Session Chair of Neural Network (part of SPLASH OOPSLA) Session Chair of Code (part of SPLASH OOPSLA) A Sound Static Analysis Approach to I/O API Migration Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Qingchao ShenShen, Qingchao Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Ashley ShengSheng, Ashley Wellesley CollegeUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
August ShiShi, August The University of Texas at AustinUnited States Understanding and Improving Flaky Test Classification
Chenghang ShiShi, Chenghang SKLP, Institute of Computing Technology, CASChina Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Chuanqi ShiShi, Chuanqi School of Computer Science and Engineering, College of Software Engineering, School of Artifical Intelligence, Southeast University ABC: Towards a Universal Code Styler through Model Merging
Jessica ShiShi, Jessica University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Qingkai ShiShi, Qingkai Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Yuanfeng ShiShi, Yuanfeng Peking UniversityChina On Abstraction Refinement for Bayesian Program Analysis
Olin ShiversShivers, Olin Northeastern UniversityUnited States Committee Member in Program Committee within the ICFP Student Research Competition-track Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Jeremy G. SiekSiek, Jeremy G. Indiana UniversityUnited States Committee Member in Distinguished Papers Committee for ICFP 2025 Session Chair of Gradual Typing and Security (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track
Cedric SiemsSiems, Cedric Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Jesse SigalSigal, Jesse University of EdinburghUnited Kingdom Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Florian SihlerSihler, Florian Ulm UniversityGermany Statically Analyzing the Dataflow of R Programs Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Robert SimmonsSimmons, Robert IndependentUnited States Committee Member in Program Commitee within the SPLASH -E-track
Abhishek Kr SinghSingh, Abhishek Kr IIIT HyderabadIndia Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Avaljot SinghSingh, Avaljot UIUCUnited States Automated Verification of Soundness of DNN Certifiers
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMware ResearchUnited States Automated Verification of Soundness of DNN Certifiers Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Satnam SinghSingh, Satnam IndependentUnited States Functional Programming for Hardware Design
Somesh SinghSingh, Somesh Siemens EDAFrance Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Vidush SinghalSinghal, Vidush Purdue UniversityUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
A. Prasad SistlaSistla, A. Prasad University of Illinois at Chicago Checking $\delta$-Satisfiability of Reals with Integrals
KC SivaramakrishnanSivaramakrishnan, KC IIT Madras and TaridesIndia Diversity Co-Chair in Organizing Committee for ICFP 2025 Diversity Co-Chair in Steering Committee for ICFP 2025 Session Chair of Implementation (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Verification 3 (part of SPLASH OOPSLA) Automatically Verifying Replication-aware Linearizability Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track A guided tour through Oxidized OCaml
Aishwarya SivaramanSivaraman, Aishwarya Meta Synthesizing Implication Lemmas for Interactive Theorem Proving
Kugesan SivasothynathanSivasothynathan, Kugesan Jaseci Labs MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Dang SixuanSixuan, Dang Duke University Agora: Trust Less and Open More in Verification for Confidential Computing
Opale SjöstedtSjöstedt, Opale Imperial College London Compositional Symbolic Execution for the Next 700 Memory Models
Philipp SlusallekSlusallek, Philipp DFKI, GermanyGermany im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
Yannis SmaragdakisSmaragdakis, Yannis University of AthensGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Peepco: Batch-Based Consistency Optimization
Thomas SomersSomers, Thomas Radboud University Nijmegen Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Dowon SongSong, Dowon Korea UniversitySouth Korea Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
Fu SongSong, Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software TechnologyChina Verification of Bit-Flip Attacks against Quantized Neural Networks
Jiaxin SongSong, Jiaxin University of Illinois at Urbana-ChampaignUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Wei SongSong, Wei Nanjing University of Science and TechnologyChina DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Yahui SongSong, Yahui Standard Chartered BankSingapore Committee Member in ICFP Programme Committee within the ICFP Papers-track
Tyler SorensenSorensen, Tyler Microsoft Research and University of California at Santa CruzUnited States SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Skye SossSoss, Skye University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Thodoris SotiropoulosSotiropoulos, Thodoris ETH ZurichSwitzerland Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Matthew SotoudehSotoudeh, Matthew Stanford University Pathological Cases for a Class of Reachability-Based Garbage Collectors
Robert SouléSoulé, Robert Yale University A Language for Quantifying Quantum Network Behavior
Vimala SoundarapandianSoundarapandian, Vimala IIT MadrasIndia Automatically Verifying Replication-aware Linearizability
Janek SpadernaSpaderna, Janek University of Freiburg, Germany Borrowing From Session Types
Arnaud SpiwackSpiwack, Arnaud TweagFrance Destination calculus: A linear λ-calculus for purely functional memory writes
Caleb StanfordStanford, Caleb University of California, DavisUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Jonathan Lindegaard StarupStarup, Jonathan Lindegaard Denmark Qualified Types with Boolean Algebras
Fynn StebelStebel, Fynn Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Maarten SteevensSteevens, Maarten Ghent University, BelgiumBelgium MIO: Multiverse Debugging in the face of Input/Output
Leo StefanescoStefanesco, Leo University of CambridgeUnited Kingdom Session Chair of Separation Logic (part of ICFP Papers) Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting
Jonathan SterlingSterling, Jonathan University of CambridgeUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Michel SteuwerSteuwer, Michel Technische Universität BerlinGermany Multiple Resumptions and Local Mutable State, Directly
Sam StitesStites, Sam Northeastern UniversityUnited States Multi-Language Probabilistic Programming
Quentin StiévenartStiévenart, Quentin Université du Québec à MontréalCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Filip StrömbäckStrömbäck, Filip Linköping UniversitySweden Continuations for All: Language Design Considerations for Accessible Continuations
Felix StutzStutz, Felix University of Luxembourg, Luxembourg Characterizing Implementability of Global Protocols with Infinite States and Data Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Zhendong SuSu, Zhendong ETH ZurichSwitzerland The Quest Toward that Perfect Compiler Validating Soundness and Completeness in Pattern-Match Coverage Analyzers An Empirical Study of Bugs in the rustc Compiler API-guided Dataset Synthesis to Finetune Large Code Models
Chamika SudusingheSudusinghe, Chamika University of Illinois at Urbana-Champaign GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Tianxiang SuiSui, Tianxiang Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Yulei SuiSui, Yulei University of New South WalesAustralia Efficient Abstract Interpretation via Selective Widening
Alexander J. SummersSummers, Alexander J. University of British ColumbiaCanada Session Chair of Rust (part of SPLASH OOPSLA) Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Chengnian SunSun, Chengnian University of WaterlooCanada Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jun SunSun, Jun Singapore Management UniversitySingapore Correct-By-Construction: Certified Individual Fairness through Neural Network Training Verification of Bit-Flip Attacks against Quantized Neural Networks Fuzzing C++ Compilers via Type-Driven Mutation
Maolin SunSun, Maolin Nanjing UniversityChina Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Yaozhu SunSun, Yaozhu National Institute of InformaticsJapan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
Vaishnavi SundararajanSundararajan, Vaishnavi IIT DelhiIndia Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Vijay SundaresanSundaresan, Vijay IBM CanadaCanada CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Shiv SundramSundram, Shiv Stanford University REPTILE: Performant Tiling of Recurrences
Chenyao SuoSuo, Chenyao Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Milijana SurbatovichSurbatovich, Milijana University of Maryland Session Chair of Women in PL Dinner (part of ICFP Diversity, Equity, and Inclusion) Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Steering Committee Chair in Steering Committee for ICFP 2025 Committee Member in ICFP Programme Committee within the ICFP Papers-track
Wouter SwierstraSwierstra, Wouter Utrecht University, NetherlandsNetherlands Member at large in Steering Committee for ICFP 2025 First-Order Laziness
T Marco T MorazanT Morazan, Marco Seton Hall UniversityUnited States Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Nicolas TabareauTabareau, Nicolas InriaFrance Robust Dynamic Embedding for Gradual Typing Incremental Certified Programming
Gourav TakharTakhar, Gourav Indian Institute of Technology - KanpurIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Jean-Pierre TalpinTalpin, Jean-Pierre INRIA, France HpC: A Calculus for Hybrid and Mobile Systems
Gang (Gary) TanTan, Gang (Gary) Pennsylvania State UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Grace TanTan, Grace National University of Singapore Evolving How We Teach Memory Models
Guangming TanTan, Guangming Chinese Academy of Sciences(CAS) Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Lin TanTan, Lin Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shangyin TanTan, Shangyin University of California, BerkeleyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Tian TanTan, Tian Nanjing UniversityChina Two Approaches to Fast Bytecode Frontend for Static Analysis
Yudai TanabeTanabe, Yudai Institute of Science TokyoJapan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Dixin TangTang, Dixin University of Texas Austin Homomorphism Calculus for User-Defined Aggregations
Lingjia TangTang, Lingjia University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Wenhao TangTang, Wenhao The University of EdinburghUnited Kingdom Modal Effect Types
Yutian TangTang, Yutian University of Glasgow, United KingdomUnited Kingdom Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Swamit TannuTannu, Swamit University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures Compiling Quantum Circuits
Éric TanterTanter, Éric University of ChileChile Robust Dynamic Embedding for Gradual Typing Incremental Certified Programming
Muhammad Usman TariqTariq, Muhammad Usman Stanford University REPTILE: Performant Tiling of Recurrences
Joseph TassarottiTassarotti, Joseph New York UniversityUnited States Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
Christine TassonTasson, Christine Sorbonne Université — LIP6France Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ross TateTate, Ross Independent Researcher and ConsultantUnited States Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Manas ThakurThakur, Manas IIT BombayIndia CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Shriya ThakurThakur, Shriya University of Massachusetts LowellUnited States Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Michelle ThalakotturThalakottur, Michelle Northeastern UniversityUnited States Student Volunteer Co-Chair in Organizing Committee for ICFP 2025
Suhas ThalankiThalanki, Suhas Carnegie Mellon University Debugging WebAssembly? Put some Whamm on it!
Peter ThiemannThiemann, Peter University of FreiburgGermany Associate Chair in ICFP Programme Committee within the ICFP Papers-track Session Chair of Tuesday ICFP Keynote (part of ICFP Keynotes) Session Chair of Proofs (part of SPLASH OOPSLA) Borrowing From Session Types
Thore ThießenThießen, Thore University of Münster Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
William ThomasThomas, William University of Kansas Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yongqiang TianTian, Yongqiang Monash UniversityHong Kong SAR China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Matthias TichyTichy, Matthias Ulm UniversityGermany Statically Analyzing the Dataflow of R Programs Waddle: A Serious Game to Teach Writing, Reading, and Debugging Programs
Eli TilevichTilevich, Eli Virginia TechUnited States Committee Member in Program Commitee within the SPLASH -E-track
Amin TimanyTimany, Amin Aarhus UniversityDenmark Reasoning about Weak Isolation Levels in Separation Logic
Christopher Steven TimperleyTimperley, Christopher Steven Carnegie Mellon UniversityUnited States ROSpec: A Domain-Specific Language for ROS-based Robot Software
Tanmay TirpankarTirpankar, Tanmay University of Utah Translation Validation for LLVM's AArch64 Backend
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited States Unveiling Heisenbugs with Diversified Execution Debugging WebAssembly? Put some Whamm on it! WebAssembly Research Tools Tutorial
Shrey TiwariTiwari, Shrey Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Ryan TjoaTjoa, Ryan University of Washington; Jane StreetUnited States Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States ICFP '26 General Chair in Steering Committee for ICFP 2025 ICFP 2026 Announcement
Bernardo ToninhoToninho, Bernardo Instituto Superior Técnico - University of LisbonPortugal Fusing Session-Typed Concurrent Programming into Functional Programming
Bernardo ToninhoToninho, Bernardo NOVA-LINCS; Nova University of LisbonPortugal Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Cassia TorczonTorczon, Cassia University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Matías ToroToro, Matías University of ChileChile Robust Dynamic Embedding for Gradual Typing Committee Member in ICFP Programme Committee within the ICFP Papers-track Flexible and Expressive Typed Path Patterns for GQL
Laurence TrattTratt, Laurence King's College LondonUnited Kingdom Garbage Collection for Rust: The Finalizer Frontier
Christoph TreudeTreude, Christoph Singapore Management UniversitySingapore Reproducibility Debt in Scientific Software
Conan TruongTruong, Conan University of California, Irvine Towards Verifying Crash Consistency
Yi-Zhen TsaiTsai, Yi-Zhen University of California, Riverside Hambazi: Spatial Coordination Synthesis for Augmented Reality
Stelios TsampasTsampas, Stelios University of Southern DenmarkDenmark Bialgebraic Reasoning on Stateful Languages CRDT Emulation, Simulation, and Representation Independence Big Steps in Higher-Order Mathematical Operational Semantics
Ilias TsatirisTsatiris, Ilias DedaubGreece Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Saar Tzour-ShadayTzour-Shaday, Saar Technion – Israel Institute of TechnologyIsrael Mini-Batch Robustness Verification of Deep Neural Networks
U Thien UdomsrirungruangUdomsrirungruang, Thien University of Oxford qblaze: An Efficient and Scalable Sparse Quantum Simulator
Hiroshi UnnoUnno, Hiroshi Tohoku UniversityJapan Committee Member in ICFP Programme Committee within the ICFP Papers-track On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Henning UrbatUrbat, Henning Friedrich-Alexander University Erlangen-NürnbergGermany Session Chair of Semantics (part of ICFP Papers) Bialgebraic Reasoning on Stateful Languages
V Jan VahrenholdVahrenhold, Jan University of MünsterGermany Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Rishikesh VaishnavVaishnav, Rishikesh Deducteam, LMF, ENS Paris-Saclay, INRIAFrance Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Nachiappan ValliappanValliappan, Nachiappan University of EdinburghUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Isaac van Bakelvan Bakel, Isaac ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Mark van den Brandvan den Brand, Mark Eindhoven University of TechnologyNetherlands Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Guy Van den BroeckVan den Broeck, Guy University of California at Los Angeles Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Jacob Van GeffenVan Geffen, Jacob Veridise Inc. Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Sushen VangeepuramVangeepuram, Sushen Iowa State University Embedding Quantum Program Verification into Dafny
Alexa VanHattumVanHattum, Alexa Wellesley CollegeUnited States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Vasco T. VasconcelosVasconcelos, Vasco T. LASIGE, University of LisbonPortugal Borrowing From Session Types
Martin VechevVechev, Martin ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Andreas VenerisVeneris, Andreas University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Hristo VenevVenev, Hristo INSAIT, Sofia University "St. Kliment Ohridski"Bulgaria qblaze: An Efficient and Scalable Sparse Quantum Simulator
Vasudev VikramVikram, Vasudev Carnegie Mellon UniversityUnited States Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Cosmo ViolaViola, Cosmo University of Illinois Urbana-Champaign Proof Repair across Quotient Type Equivalences
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States Checking $\delta$-Satisfiability of Reals with Integrals
Yakir VizelVizel, Yakir Technion—Israel Institute of TechnologyIsrael Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arya VohraVohra, Arya University of Chicago Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Finn VoichickVoichick, Finn University of MarylandUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Compositional Quantum Control Flow with Efficient Compilation in Qunity
David VoigtVoigt, David University of Tübingen Dynamic Wind for Effect Handlers
Domagoj VrgočVrgoč, Domagoj Pontificia Universidad Católica de Chile & IMFD Chile Flexible and Expressive Typed Path Patterns for GQL
W Philip WadlerWadler, Philip IOG; University of EdinburghUnited Kingdom A simple blame calculus for explicit nulls Session Chair of Parametricity (part of ICFP Papers)
Andrew WagnerWagner, Andrew Northeastern UniversityUnited States From Linearity to Borrowing
Gijs WalravensWalravens, Gijs Eindhoven University of Technology Personalization of Programming Education: An NLP-based Bi-dimensional Classification of Programming Exercises
Michael WalterWalter, Michael Ruhr-Universität Bochum QbC: Quantum Correctness by Construction
Qianyong WanWan, Qianyong University of Hong KongChina Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Bo WangWang, Bo Beijing Jiaotong UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Chao WangWang, Chao University of Southern CaliforniaUnited States Probabilistic Inference for Datalog with Correlated Inputs
Di WangWang, Di Peking UniversityChina Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Hanzhang WangWang, Hanzhang Fudan University, ChinaChina JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Jianrong WangWang, Jianrong Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Jiawei WangWang, Jiawei UNSW Efficient Abstract Interpretation via Selective Widening
Jingbo WangWang, Jingbo Purdue University Probabilistic Inference for Datalog with Correlated Inputs
Ke WangWang, Ke Peking University Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Linzhang WangWang, Linzhang Nanjing University Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Peixin WangWang, Peixin East China Normal University Structural Abstraction and Refinement for Probabilistic Programs
Ruixin WangWang, Ruixin Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Shengyi WangWang, Shengyi Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Shiqi WangWang, Shiqi AWS AI LabsUnited States UTFix: Change Aware Unit Test Repairing using LLM
Shuai WangWang, Shuai Hong Kong University of Science and TechnologyChina Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines API-guided Dataset Synthesis to Finetune Large Code Models Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Shuling WangWang, Shuling Institute of Software, Chinese Academy of Sciences HpC: A Calculus for Hybrid and Mobile Systems
Wenwen WangWang, Wenwen University of GeorgiaUnited States JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenxi WangWang, Wenxi University of VirginaUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
XiaoFeng WangWang, XiaoFeng Nanyang Technological University Agora: Trust Less and Open More in Verification for Confidential Computing
Xinyu WangWang, Xinyu University of MichiganUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Yongjia WangWang, Yongjia College of Intelligence and Computing, Tianjin University DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Yongzhi WangWang, Yongzhi Xidian University HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Yu WangWang, Yu Nanjing UniversityChina Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yuning WangWang, Yuning Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Zhuangda WangWang, Zhuangda Xiamen UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Zihan WangWang, Zihan The University of Queensland and CSIRO's Data61Australia Convex Hull Approximation for Activation Functions
Ziteng WangWang, Ziteng University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Homomorphism Calculus for User-Defined Aggregations
Kazuki WatanabeWatanabe, Kazuki National Institute of Informatics; SOKENDAIJapan A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Doctoral Symposium Chair in Organizing Committee for ICFP 2025 Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track WebAssembly Research Tools Tutorial
Joe WattWatt, Joe *Institute for Infocomm Research, ASTARSingapore** Student Volunteer Co-Chair in Organizing Committee for ICFP 2025
Anjiang WeiWei, Anjiang Stanford UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Guannan WeiWei, Guannan Tufts UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ivan WeiWei, Ivan University of Michigan Incremental Bidirectional Typing via Order Maintenance
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Hongbo WenWen, Hongbo University of California, Santa Barbara & Riema Labs Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Zhongzhen WenWen, Zhongzhen Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Sam WestrickWestrick, Sam New York UniversityUnited States Publicity Chair in Organizing Committee for ICFP 2025 Publicity Chair in Steering Committee for ICFP 2025
Leo WhiteWhite, Leo Jane StreetUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track Modal Effect Types
John WickersonWickerson, John Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Thomas WiesWies, Thomas New York UniversityUnited States Abstract Interpretation of Temporal Safety Effects of Higher Order Programs Characterizing Implementability of Global Protocols with Infinite States and Data
Graham WilliamsWilliams, Graham Australian National University Reproducibility Debt in Scientific Software
Richard WillieWillie, Richard National University of Singapore View Types in Rust
Christian WimmerWimmer, Christian Amazon Web ServicesUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Daniel Winograd-CortWinograd-Cort, Daniel Nectry Inc.United States Sponsorship Co-Chair in Organizing Committee for ICFP 2025 Sponsorship Co-Chair in Organizing Committee for ICFP 2025 Industrial Relations Chair in Steering Committee for ICFP 2025
Théo WinterhalterWinterhalter, Théo INRIAFrance SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jaeyeon WonWon, Jaeyeon MIT The Continuous Tensor Abstraction: Where Indices are Real
Jotham WongWong, Jotham National University of Singapore, SingaporeSingapore Evolving How We Teach Memory Models
Wai Kin WongWong, Wai Kin Hong Kong University of Science and Technology Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Daniel WrightWright, Daniel University of Surrey Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Tobias WrigstadWrigstad, Tobias Uppsala UniversitySweden Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Daoyuan WuWu, Daoyuan Lingnan UniversityHong Kong SAR China Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines API-guided Dataset Synthesis to Finetune Large Code Models
Jiangchang WuWu, Jiangchang Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Ming WuWu, Ming Shanghai Tree-Graph Blockchain Research Institute HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Rongxin WuWu, Rongxin Xiamen UniversityChina TailTracer: Continuous Tail Tracing for Production Use
Shushu WuWu, Shushu Shanghai Jiao Tong University Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
Xiwei WuWu, Xiwei Shanghai Jiao Tong UniversityChina Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
X Dongwei XiaoXiao, Dongwei Hong Kong University of Science and TechnologyHong Kong SAR China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Junmin XiaoXiao, Junmin Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Linjie XiaoXiao, Linjie Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Linna XieXie, Linna Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Ningning XieXie, Ningning University of TorontoCanada Multi-stage Programming with Splice Variables Committee Member in ICFP Programme Committee within the ICFP Papers-track
Ruifeng XieXie, Ruifeng Peking University Effectful Lenses: There and Back with Different Monads
Zifan XieXie, Zifan Huazhong University of Science and TechnologyChina Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Jimmy XinXin, Jimmy The University of Texas at Austin Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong XinXin, Yutong The University of Texas at Austin Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Chris XiongXiong, Chris Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust
Yingfei XiongXiong, Yingfei Peking UniversityChina Session Chair of Synthesis 1 (part of SPLASH OOPSLA) Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Amanda XuXu, Amanda University of Wisconsin-Madison Dependency-Aware Compilation for Surface Code Quantum Architectures Checking Observational Correctness of Database Systems Compiling Quantum Circuits
Baowen XuXu, Baowen Nanjing University An Empirical Study of Bugs in the rustc Compiler
Han XuXu, Han Princeton UniversityUnited States Liberating Merges via Apartness and Guarded Subtyping
Jiexiao XuXu, Jiexiao University of Washington Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Xiangzhe XuXu, Xiangzhe Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Xiong XuXu, Xiong Institute of Software, Chinese Academy of Sciences HpC: A Calculus for Hybrid and Mobile Systems
Yichen XuXu, Yichen EPFL What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Zhenyang XuXu, Zhenyang University of WaterlooCanada Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Jingling XueXue, Jingling University of New South WalesAustralia Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Runze XueXue, Runze University of Michigan; University of Cambridge; Indiana UniversityUnited States Notions of Stack-manipulating Computation and Relative Monads
Xu XueXue, Xu The University of Hong Kong Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Frex: Dependently Typed Algebraic Simplification
Chenyuan YangYang, Chenyuan University of Illinois Urbana-ChampaignUnited States AutoVerus: Automated Proof Generation for Rust Code
Fan YangYang, Fan Microsoft Research Asia AutoVerus: Automated Proof Generation for Rust Code
Min YangYang, Min Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Minghui YangYang, Minghui OPPO ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Sen YangYang, Sen Yale University Agora: Trust Less and Open More in Verification for Confidential Computing
Yibiao YangYang, Yibiao Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Yixin YangYang, Yixin Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ziyi YangYang, Ziyi National University of SingaporeSingapore Inductive Synthesis of Inductive Heap Predicates
Jianan YaoYao, Jianan University of Toronto AutoVerus: Automated Proof Generation for Rust Code
Peisen YaoYao, Peisen Zhejiang UniversityChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Wenjia YeYe, Wenjia National University of SingaporeSingapore Flexible and Expressive Typed Path Patterns for GQL
Pen-Chung YewYew, Pen-Chung University of Minnesota at Twin CitiesUnited States JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Kwangkeun YiYi, Kwangkeun Seoul National University React-tRace: A Semantics for Understanding React Hooks
Xizhe YinYin, Xizhe Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Irene YoonYoon, Irene InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml Committee Member in ICFP Programme Committee within the ICFP Papers-track
Taeyoung YoonYoon, Taeyoung Seoul National University Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Brent YorgeyYorgey, Brent Hendrix CollegeUnited States You could have invented Fenwick trees
Nobuko YoshidaYoshida, Nobuko University of OxfordUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Shu-Hung YouYou, Shu-Hung Institute of Information Science, Academia Sinica, TaiwanTaiwan Contract System Metatheories à la Carte: A Transition-System View of Contracts
David YoungYoung, David University of Kansas, USA A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Neringa YoungYoung, Neringa Lithuania SIGPLAN Conference Manager in Organizing Committee for ICFP 2025
Nengkun YuYu, Nengkun Stony Brook University, USAUnited States Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Liang YuanYuan, Liang Chinese Academy of Sciences Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Peng YuanYuan, Peng Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Shenghao YuanYuan, Shenghao Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Yongwei YuanYuan, Yongwei Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yueming YuanYuan, Yueming University of Illinois Urbana-Champaign SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Zhou YuanyuanYuanyuan, Zhou UCSD On the Impact of Formal Verification on Software Development Laurel: Unblocking Automated Verification with Large Language Models
Insu YunYun, Insu KAIST Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Z Yannick ZakowskiZakowski, Yannick InriaFrance Structural temporal logic for mechanized program verification Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Lucas ZavaliaZavalia, Lucas Florida State University TallahasseeUnited States A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Opportunistically Parallel Lambda Calculus Structural temporal logic for mechanized program verification
Stefan ZetzscheZetzsche, Stefan AmazonUnited Kingdom Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Thomas ZeumeZeume, Thomas Ruhr University BochumGermany Detecting and explaining (in-)equivalence of context-free grammars
Bohua ZhanZhan, Bohua Huawei Technologies Co., Ltd. HpC: A Calculus for Hybrid and Mobile Systems
Naijun ZhanZhan, Naijun Peking University HpC: A Calculus for Hybrid and Mobile Systems
Chaoyue ZhangZhang, Chaoyue Nanjing UniversityChina Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Charles ZhangZhang, Charles The Hong Kong University of Science and TechnologyChina Session Chair of Friday SPLASH Keynote (part of SPLASH Keynotes) Session Chair of TOPLAS and Remote (part of SPLASH OOPSLA) SPLASH Awards General Chair Report
Cheng ZhangZhang, Cheng Worcester Polytechnic InstituteUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Chengyu ZhangZhang, Chengyu ETH Zurich Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Danfeng ZhangZhang, Danfeng Duke UniversityUnited States Agora: Trust Less and Open More in Verification for Confidential Computing
Fan ZhangZhang, Fan Yale University Agora: Trust Less and Open More in Verification for Confidential Computing
Jialu ZhangZhang, Jialu University of WaterlooCanada Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Mengxiao ZhangZhang, Mengxiao Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Nuda ZhangZhang, Nuda University of Michigan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited States Fast Constraint Synthesis for C++ Function Templates Chair in Organizing Committee within the SPLASH Posters-track
Ruihan ZhangZhang, Ruihan Singapore Management University (SMU) Correct-By-Construction: Certified Individual Fairness through Neural Network Training
Shuhao ZhangZhang, Shuhao Peking UniversityChina Tunneling Through the Hill: Multi-Way Intersection for Version-Space Algebras in Program Synthesis
Tian ZhangZhang, Tian Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Tianyi ZhangZhang, Tianyi Purdue UniversityUnited States Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Weihua ZhangZhang, Weihua Fudan UniversityChina JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Wenmeng ZhangZhang, Wenmeng College of Computer Science and Technology, National University of Defense Technology, Changsha, China Multi-Modal Sketch-based Behavior Tree Synthesis
Xiangyu ZhangZhang, Xiangyu Purdue UniversityUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Xiaojing ZhangZhang, Xiaojing Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Xin ZhangZhang, Xin Peking UniversityChina Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences On Abstraction Refinement for Bayesian Program Analysis
Xing ZhangZhang, Xing Peking UniversityChina Fuzzing C++ Compilers via Type-Driven Mutation
Yedi ZhangZhang, Yedi National University of Singapore Verification of Bit-Flip Attacks against Quantized Neural Networks
Yi ZhangZhang, Yi Nanjing UniversityChina Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yifan ZhangZhang, Yifan Peking UniversityChina On Abstraction Refinement for Bayesian Program Analysis
Ying ZhangZhang, Ying Wake Forest UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yiyu ZhangZhang, Yiyu Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Compiling with Generating Functions Zero-Overhead Lexical Effect Handlers
Yuan ZhangZhang, Yuan Fudan UniversityChina ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Zhaoyang ZhangZhang, Zhaoyang The Hong Kong University of Science and TechnologyHong Kong SAR China A Sound Static Analysis Approach to I/O API Migration
Zhuoruo ZhangZhang, Zhuoruo Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Ziqi ZhangZhang, Ziqi University of Illinois Urbana-ChampaignChina Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Pinhan ZhaoZhao, Pinhan University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Wenyu ZhaoZhao, Wenyu Australian National UniversityAustralia Advancing Performance via a Systematic Application of Research and Industrial Best Practice Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Yongwang ZhaoZhao, Yongwang Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Yubo ZhaoZhao, Yubo Shanghai Jiao Tong University Binary Cryptographic Function Identification via Similarity Analysis with Path-insensitive Emulation
Zhongkai ZhaoZhao, Zhongkai National University of Singapore Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Linus ZhengZheng, Linus University of Texas at Austin Homomorphism Calculus for User-Defined Aggregations
Xusheng ZhiZhi, Xusheng University of Wisconsin-MadisonUnited States (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
Byron ZhongZhong, Byron University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Sizhe ZhongZhong, Sizhe The Hong Kong University of Science and Technology A Sound Static Analysis Approach to I/O API Migration
Zhineng ZhongZhong, Zhineng Key Laboratory of High-Confidence Software Technologies (MOE), School of Computer Science, Peking University Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Diyu ZhouZhou, Diyu Peking University A Sound Static Analysis Approach to I/O API Migration
Litao ZhouZhou, Litao University of Hong KongChina Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Quan ZhouZhou, Quan Penn State University Agora: Trust Less and Open More in Verification for Confidential Computing
Xiangyu ZhouZhou, Xiangyu University of Michigan Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yanqi ZhouZhou, Yanqi Google SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Yuming ZhouZhou, Yuming Nanjing UniversityChina Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Zhe ZhouZhou, Zhe Purdue University We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Zhichao ZhouZhou, Zhichao School of Information Science and Technology, ShanghaiTech UniversityChina Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ziqiao ZhouZhou, Ziqiao Microsoft ResearchUnited States AutoVerus: Automated Proof Generation for Rust Code
He ZhuZhu, He Rutgers University, USA Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Jun ZhuZhu, Jun Nankai University Adaptive Shielding via Parametric Safety Proofs
Qing ZhuZhu, Qing Ant Group MetaKernel: Enabling Efficient Encrypted Neural Network Inference Through Unified MVM and Convolution
Siyuan ZhuZhu, Siyuan Peking University, China Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Oleksandr ZinenkoZinenko, Oleksandr Brium Sound and Modular Activity Analysis for Automatic Differentiation in MLIR Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Li ZongjieZongjie, Li Hong Kong University of Science and TechnologyChina API-guided Dataset Synthesis to Finetune Large Code Models
Damien ZuffereyZufferey, Damien SonarSourceSwitzerland Characterizing Implementability of Global Protocols with Infinite States and Data
Zhiqiang ZuoZuo, Zhiqiang Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use
Aron ZwaanZwaan, Aron Delft University of TechnologyNetherlands Language-Parametric Reference Synthesis
Š Artjoms ŠinkarovsŠinkarovs, Artjoms University of Southampton Committee Member in Program Committee within the ICFP Student Research Competition-track Correctness Meets Performance: From Agda to Futhark

ICFP 2025 Contributors

Results (1230)

Tracks

ICFP/SPLASH 2025

Co-hosted Conferences

Workshops

Co-hosted Symposia