ICFP/SPLASH 2025 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1913)

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 Committee Member in Program Committee within the Haskell-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 Scheme and New Frontiers for Language Design Exotic Uses of Continuations Pushing the Information-Theoretic Limits of Random Access Lists Committee Member in Program Committee within the ML Family Workshop-track Program Co-Chair in Organizing Committee within the miniKanren-track
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 Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
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 Steering Committee Member in Steering Committee for SPLASH 2025 [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track 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 2-Functoriality of Initial Semantics, and Applications Committee Member in Program Committee within the ICFP Student Research Competition-track
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
Cons AhsAhs, Cons Meta Committee Member in Program Committee within the Erlang-track
Marat AkhinAkhin, Marat JetBrainsNetherlands Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Shoaib AkramAkram, Shoaib Australian National UniversityAustralia Closing Welcome Co-chair in Program Committee within the VMIL-track Co-chair in Organizing Committee within the VMIL-track SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Compiling Quantum Circuits Dependency-Aware Compilation for Surface Code Quantum Architectures Checking Observational Correctness of Database Systems
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference Unfolding Expressions for Gradual Verification Gradual Verification: Assuring Software Incrementally Discussion Usability Barriers for Liquid Types (Summary of Published Work) Committee Member in Organizing Committee within the HATRA-track
Mark W. AldrichAldrich, Mark W. Tufts UniversityUnited States RestPi: Path-Sensitive Type Inference for REST APIs
Karim AliAli, Karim NYU Abu DhabiUnited Arab Emirates Committee Member in Program Committee within the SAS -track
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
Roberto AloiAloi, Roberto Meta A stop-the-world debugger for Erlang (and the BEAM)
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 The Modular Imperative: Rethinking LLMs for Maintainable Software Beyond Cons: Purely Relational Data Structures Committee Member in Program Committee within the FUNARCH-track
Torben AmtoftAmtoft, Torben Kansas State University More than a Colleague: Celebrating Olivier’s Impact
Junwen AnAn, Junwen Singapore LLM-assisted Dialect-Agnostic SQL Query Parsing
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
Carolyn Jane AndersonAnderson, Carolyn Jane Wellesley CollegeUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Roy AngAng, Roy University of Cambridge Spatial Programming for Environmental Monitoring
Zhendong AngAng, Zhendong National University of Singapore Ranking Formal Specifications using LLMs
Sebastian AngelAngel, Sebastian University of PennsylvaniaUnited States Structural temporal logic for mechanized program verification
Alexandros Emmanouil AntonakakisAntonakakis, Alexandros Emmanouil ICS-FORTH & University of Crete MaTSa: Race Detection in Java
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
Mizuki ArataArata, Mizuki None LunarML: From Standard ML to Scripting Languages
Vincenzo ArceriArceri, Vincenzo University of Parma, ItalyItaly Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Blair ArchibaldArchibald, Blair University of GlasgowUnited Kingdom TideScript: A Domain Specific Language for Peptide Chemistry
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
Chris ArmstrongArmstrong, Chris Australia smaws: An AWS SDK for OCaml
Michael ArntzeniusArntzenius, Michael UC BerkeleyUnited States Finite functional programming via graded effects and relevance types Fair intersection of seekable iterators
Stavros AronisAronis, Stavros Erlang Solutions, SwedenGreece Committee Member in Program Committee within the Erlang-track
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Defining Algebraic Effects and Handlers via Trails and Metacontinuations Programme Committee in Program Committee within the OlivierFest-track Session Chair of Morning Paper Session (part of SPLASH -E) Committee Member in Program Commitee within the SPLASH -E-track OCaml Blockly
Flavio AscariAscari, Flavio University of Pisa Revealing Sources of (Memory) Errors via Backward Analysis
Eric AtkinsonAtkinson, Eric Binghamton University Artifact Evaluation Co-Chair in Organizing Committee for SPLASH 2025 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track OOPSLA Artifact Awards
Skyler AustenAusten, Skyler Brown University Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Charles AverillAverill, Charles University of Texas at DallasUnited States The Proof Must Go On: Formal Methods in the Theater of Secure Software Development of the Future
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 H. Azevedo de AmorimAzevedo de Amorim, Pedro H. University of OxfordUnited Kingdom Substructural Weakest Preconditions in Fibrations
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 Generic Reduction-Based Interpreters Programme Committee in Program Committee within the OlivierFest-track Language-Parametric Reference Synthesis
Jakub BachurskiBachurski, Jakub University of CambridgeUnited Kingdom Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Kyungmin BaeBae, Kyungmin POSTECHSouth Korea Formal Analysis of Networked PLC Controllers Interacting with Physical Environments Committee Member in Program Committee within the SAS -track
Lorenzo BafunnoBafunno, Lorenzo University of Torino, Italy A typed approach to ontology manipulation (experience report)
Shiv Kiran BagathiBagathi, Shiv Kiran Indian Institute of Technology Bombay ScalaF: Functional Refactoring Suggestions for Scala
Thomas BAGRELBAGREL, Thomas Tweag, LORIA/INRIA Destination calculus: A linear λ-calculus for purely functional memory writes
Patrick BahrBahr, Patrick IT University of CopenhagenDenmark The Calculated Typer (Functional Pearl) Committee Member in Program Committee within the Haskell-track
Alexander BaiBai, Alexander New York UniversityUnited States Video Chair in AV Committee for ICFP/SPLASH 2025 Video Chair in Organizing Committee for ICFP/SPLASH 2025 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 Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse
Guangdong BaiBai, Guangdong University of QueenslandAustralia Convex Hull Approximation for Activation Functions
Thibaut BalabonskiBalabonski, Thibaut LMF, CNRS, Université Paris-Saclay How to Fold a Tree: Programming Exercises on Calder’s Mobiles Programme Committee in Program Committee within the OlivierFest-track
Hrishikesh BalakrishnanBalakrishnan, Hrishikesh University of Illinois Urbana-Champaign FO-Complete Program Verification for Heap Logics
Patrycja BalikBalik, Patrycja University of WrocławPoland Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction
Lucas BangBang, Lucas Harvey Mudd College PLMW Co-Chair in Organizing Committee for ICFP/SPLASH 2025 PLMW Co-Chair in Organizing Committee for SPLASH 2025 [CANCELED] Adaptive Search Synthesis as a Recursion Scheme PLMW Welcome Committee Member in Program Committee within the PLMW @ ICFP/SPLASH-track
Elisa BaniassadBaniassad, Elisa University of British ColumbiaCanada Committee Member in Program Commitee within the SPLASH -E-track
Ajay BansalBansal, Ajay Arizona State University Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren
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
Chinmayi Prabhu BaramashetruBaramashetru, Chinmayi Prabhu University of Oslo Towards Modelling and Verification of Coupler Behaviour in Climate Models Committee Member in Program Committee within the PROPL-track
Mikhail BarashBarash, Mikhail University of BergenNorway Involving Students in Design and Implementation of ECMAScript (JavaScript) Proposals
Saam BaratiBarati, Saam Epic GamesUnited States On creating a virtual machine for Verse, a language for programming in a shared real-time 3D simulation
Ronita BardhanBardhan, Ronita University of Cambridge Scaling the Urban Forest: An Integrated Framework for Managing Cities by Fusing Raster and Vector Data
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance Committee Member in Program Committee within the SAS -track
Shraddha BarkeBarke, Shraddha Microsoft Research, RedmondUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track Committee Member in Program Committee within the HATRA-track
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
Earl T. BarrBarr, Earl T. University College LondonUnited Kingdom Committee Member in Program Committee within the LMPL-track
Hugo BarreiroBarreiro, Hugo École PolytechniqueFrance Constrained generation of well-typed programs (Extended Abstract) [Remote]
Clark BarrettBarrett, Clark Stanford UniversityUnited States Interactive Bit Vector Reasoning using Verified Bitblasting Lessons from Building a Hardware Compiler in Scala 3: A Practitioner Perspective
Edd BarrettBarrett, Edd King's College LondonUnited Kingdom Committee Member in Program Committee within the VMIL-track
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Committee Member in ICFP Programme Committee within the ICFP Papers-track
Antranig BasmanBasman, Antranig Raising the Floor - InternationalUnited Kingdom Committee Member in Program Committee within the SPLASH Onward! 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 ScaIR: Type-safe Compiler Framework Compatible with MLIR
Rohan BavishiBavishi, Rohan AmazonUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Review Committee within the SPLASH Student Research Competition-track
Barış BayazıtBayazıt, Barış University of Toronto A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Calvin BeckBeck, Calvin University of Pennsylvania, USACanada Accessibility Chair in Organizing Committee for ICFP/SPLASH 2025
Jonah BeckfordBeckford, Jonah DiskuvUnited States Committee Member in Program Committee within the OCaml-track
Tom BeckmannBeckmann, Tom Hasso Plattner InstituteGermany Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions Block-based Editing in a Textual World Organizer in Organizing Committee within the PAINT-track Committee Member in Program Committee within the PAINT-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 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
Viktor BenseBense, Viktor Eötvös Loránd University (ELTE) The conatural numbers form an exponential commutative semiring
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
Péter BereczkyBereczky, Péter Eötvös Loránd UniversityHungary Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Mechanised Proofs of Atom Exhaustion in Erlang
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 Committee Member in ICFP Programme Committee within the ICFP Papers-track Domain-specific tensor languages
Quentin BernetBernet, Quentin EPFL Logically Qualified Types for Scala
Gilbert BernsteinBernstein, Gilbert University of WashingtonUnited States Committee Member in Program Committee within the SPLASH FARM-track Polynomial-Time Program Equivalence for Machine Knitting
Antonia BertolinoBertolino, Antonia Gran Sasso Science InstituteItaly RuntimeSave: A Graph Database of Runtime Values
Ivan BeschastnikhBeschastnikh, Ivan The University of British ColumbiaCanada TraceLinking Implementations with their Verified Designs Debugging for Scala Control Flow DSLs
Raven BeutnerBeutner, Raven CISPA Helmholtz Center for Information Security, Germany Verifying Asynchronous Hyperproperties in Reactive Systems
Joey BevilacquaBevilacqua, Joey USI LuganoItaly TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro
Karthikeyan BhargavanBhargavan, Karthikeyan Cryspen, France A Mechanically Verified Garbage Collector for OCaml
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
Annette BieniusaBieniusa, Annette RPTU Kaiserslautern-LandauGermany PC Member in Program Committee within the SPLASH Onward! Essays-track
Dariusz BiernackiBiernacki, Dariusz University of WrocławPoland Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction Programme Committee in Program Committee within the OlivierFest-track
Baldip BijlaniBijlani, Baldip Indian Institute of Technology Kanpur Memory-Safety Verification of Open Programs With Angelic Assumptions
Angelos BilasBilas, Angelos University of Crete and FORTH, Greece MaTSa: Race Detection in Java SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Vladyslav BilykBilyk, Vladyslav Semantics-preserving Transformation of Context-free Grammars into LL(1) Form
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) Committee Member in Program Committee within the MPLR-track
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 A Mechanized Semantics for Dataflow Circuits Committee Member in ICFP Programme Committee within the ICFP Papers-track
Kelly BlincoeBlincoe, Kelly University of AucklandNew Zealand PC Member in Program Committee within the SPLASH Onward! Essays-track
Andrew BlinnBlinn, Andrew University of MichiganUnited States Syntactic Completions with Material Obligations Committee Member in Program Committee within the HATRA-track
Polina BobrovaBobrova, Polina Restoring Data Sovereignty: A Human-Centered Approach Blockchain Health Technology
Ivana BocevskaBocevska, Ivana TU Wien Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Sean BocirneaBocirnea, Sean University of British Columbia Fast and Extensible Hybrid Embeddings with Micros 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
Mathieu BoespflugBoespflug, Mathieu TweagFrance Invertible Syntax without the Tuples (Functional Pearl) Programme Committee in Program Committee within the OlivierFest-track
Rose BohrerBohrer, Rose National Institute of Advanced Industrial Science and Technology (AIST), JapanJapan Committee Member in Program Committee within the SPLASH FARM-track
Giacomo BoldiniBoldini, Giacomo Ca' Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
CF Bolz-TereickBolz-Tereick, CF Heinrich-Heine-Universität DüsseldorfGermany Tracing Just-in-time Compilation for Effects and Handlers
Joe BondBond, Joe University of Bristol, UK Authoring Tools for Transparent Climate Reporting
Michael D. BondBond, Michael D. Ohio State University Carapace: Static–Dynamic Information Flow Control in Rust Committee Member in Program Committee within the MPLR-track
Juan Camilo BonetBonet, Juan Camilo Universidad de los Andes Moving Objects and Behavior Safely in Ad hoc Networks
Daniele BonettaBonetta, Daniele VU AmsterdamNetherlands HeapBuffers: Why not just using a binary serialization format for your managed memory?
Viviana BonoBono, Viviana University of TorinoItaly A typed approach to ontology manipulation (experience report)
Tabea BordisBordis, Tabea Karlsruhe Institute of Technology X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Cândida BorgesBorges, Cândida Concert: The River Oycus
Aleksander Boruch-GruszeckiBoruch-Gruszecki, Aleksander Charles UniversityCzechia Committee Member in Organizing Committee within the IWACO-track
Raja BoujbelBoujbel, Raja OCamlProFrance Committee Member in Program Committee within the OCaml-track
Dmitri BoulytchevBoulytchev, Dmitri Saint Petersburg State UniversityRussia Session Chair of Explorations in miniKanren and Relational Programming & Panel/Discussion (part of miniKanren) An Empirical Study of Rational Tree Unification for miniKanren
Nader Boushehrinejad MoradiBoushehrinejad Moradi, Nader University of UtahUnited States Translation Validation for LLVM's AArch64 Backend
Erwan BousseBousse, Erwan Nantes UniversitéFrance Committee Member in Program Committee within the PAINT-track
Matt BovelBovel, Matt EPFL Existentialize your Generics Logically Qualified Types for Scala Existentialize your Generics Logically Qualified Types for Scala 3
Wavid BowmanBowman, Wavid University of FloridaUnited States Debugging WebAssembly? Put some Whamm on it!
William J. BowmanBowman, William J. University of British ColumbiaCanada Fast and Extensible Hybrid Embeddings with Micros PC Member in Program Committee within the SPLASH Onward! Essays-track Type-Preserving Flat Closure Optimization Type Universes as Kripke Worlds Committee Member in ICFP Programme Committee within the ICFP Papers-track Towards a Performance Comparison of Syntax and Type-Directed NbE (Extended Abstract) Committee Member in Program Committee within the HOPE-track
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany 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 Multiple Resumptions and Local Mutable State, Directly Committee Member in ICFP Programme Committee within the ICFP Papers-track Committee Member in Program Committee within the ML Family Workshop-track Committee Member in Program Committee within the ICFP Student Research Competition-track
Edwin BradyBrady, Edwin University of St. AndrewsUnited Kingdom Frex: Dependently Typed Algebraic Simplification Imperative Syntax for Dependent Types
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 Session Chair of Capabilities and ownership in Scala (part of IWACO) Session Chair of Noon (part of The Scala Workshop) Session Chair of Afternoon (part of The Scala Workshop) Session Chair of Morning (part of The Scala Workshop) Welcome to Scala'25 System Capybara: Capture Tracking for Ownership and Borrowing PC Chair in Program Committee within the The Scala Workshop-track Organizer in Organizing Committee within the The Scala Workshop-track
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 Committee Member in Program Committee within the SAS -track
Anita BuckleyBuckley, Anita USI Lugano A Language for Quantifying Quantum Network Behavior
Humphrey BurchellBurchell, Humphrey University of KentUnited Kingdom Evaluating Candidate Instructions for Reliable Program Slowdown at the Compiler Level - Towards Supporting Fine-grained Slowdown for Advanced Developer Tooling Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
Roger BurtonpatelBurtonpatel, Roger University of PennsylvaniaUnited States Rocq N'Roll Concert: RocqNRoll
Ali R. ButtButt, Ali R. Virginia Tech Memory Tiering in Python Virtual Machine
William E. ByrdByrd, William E. University of Alabama at BirminghamUnited States Committee Member in Distinguished Papers Committee for ICFP 2025 Program Co-Chair in Organizing Committee within the Scheme-track Committee Member in ICFP Programme Committee within the ICFP Papers-track Beyond Cons: Purely Relational Data Structures Program Co-Chair in Organizing Committee within the miniKanren-track
Maja BystromBystrom, Maja Bevara On Dynamic Multimedia Pipelines for Opening Browsers to New Formats
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
Lukas BöhmeBöhme, Lukas Hasso Plattner Institute, University of Potsdam, Potsdam, GermanyGermany Session Chair of Session 1 (part of PAINT) Session Chair of Session 2 (part of PAINT) Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions Block-based Editing in a Textual World Organizer in Organizing Committee within the PAINT-track
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
Yuandao CaiCai, Yuandao Hong Kong University of Science and TechnologyChina Committee Member in Program Committee within the LMPL-track
Jose CalderonCalderon, Jose Galois, Inc.United States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
José Pablo CambroneroCambronero, José Pablo Google, USAUnited States Committee Member in Review Committee within the SPLASH Student Research Competition-track
Davide CaminoCamino, Davide University of Torino, Italy A typed approach to ontology manipulation (experience report)
Marco CampionCampion, Marco INRIA & ENS Paris \| Université PSLFrance Session Chair of Abstract Interpretation (part of SAS ) Relating Distances and Abstractions: An Abstract Interpretation Perspective
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 The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics
Yiyuan CaoCao, Yiyuan Peking University Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning
Cristina CarbunaruCarbunaru, Cristina National University of Singapore, SingaporeSingapore Evolving How We Teach Memory Models
Nicolás CardozoCardozo, Nicolás Universidad de los AndesColombia Moving Objects and Behavior Safely in Ad hoc Networks Committee Member in Program Committee within the MPLR-track
Travis CardwellCardwell, Travis Well-Typed LLP Automatic C bindings generation for Haskell
Jacques CaretteCarette, Jacques McMaster UniversityCanada Committee Member in Program Committee within the SPLASH Onward! Papers-track
J. CarrCarr, J. University of ChicagoUnited States Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
Max CarrollCarroll, Max University of Cambridge Decomposable Type Highlighting for Bidirectional Type and Cast Systems
Chandler CarruthCarruth, Chandler GoogleUnited States Carbon: from C++ to Memory Safety
Chris CasinghinoCasinghino, Chris Jane Street A guided tour through Oxidized OCaml Session Chair of ML Workshop 1 (part of ML Family Workshop) Committee Member in Program Committee within the ML Family Workshop-track
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université Paris CitéFrance Polymorphic Records for Dynamic Languages Committee Member in Program Committee within the Erlang-track
Elias CastegrenCastegren, Elias Uppsala UniversitySweden Committee Member in Organizing Committee within the IWACO-track
Jonathan CastelloCastello, Jonathan University of California, Santa CruzUnited States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern CRDT Emulation, Simulation, and Representation Independence
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
Manuel ChakravartyChakravarty, Manuel Tweag & IOGNetherlands A Layered Certifying Compiler Architecture
Manuel M. T. ChakravartyChakravarty, Manuel M. T. IOHKNetherlands Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Kartik ChandraChandra, Kartik MITUnited States Gauguin, Descartes, Bayes: A Diurnal Golem's Brain 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 Steering Committee Member in Steering Committee for SPLASH 2025 Session Chair of Analysis 1 (part of SPLASH OOPSLA) Bolt-On Strong Consistency: Specification, Implementation, and Verification Committee Member in Steering Committee within the SAS -track
Rui ChangChang, Rui Zhejiang University A complete formal semantics of eBPF instruction set architecture for Solana
Arthur CharguéraudCharguéraud, Arthur InriaFrance A Core Language for Extended Pattern Matching and Binding Boolean Expressions Committee Member in Program Committee within the ML Family Workshop-track
Prantik ChatterjeeChatterjee, Prantik MathWorksIndia Memory-Safety Verification of Open Programs With Angelic Assumptions
Dr. Angela ChaudhuriChaudhuri, Dr. Angela Swasti Precision Action Towards Climate and Health (PATCH)
Chao-Hong ChenChen, Chao-Hong MetaTaiwan Gradual Metaprogramming
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 CG-Bench: Can Language Models Assist Call Graph Construction in the Real World?
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
Jimmy ChenChen, Jimmy Stanford University [CANCELED] Adaptive Search Synthesis as a Recursion Scheme
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 Committee Member in Program Committee within the LMPL-track
Junjie ChenChen, Junjie Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure Fuzzing C++ Compilers via Type-Driven Mutation
Liang-Ting ChenChen, Liang-Ting Academia SinicaTaiwan From Datatype-Generic Programming to Language-Generic Programming
Liqian ChenChen, Liqian NUDTChina Committee Member in Program Committee within the SAS -track
Menglong ChenChen, Menglong Nanjing UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Mingshuai ChenChen, Mingshuai Zhejiang UniversityChina Preguss: It Analyzes, It Specifies, It Verifies
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
Tianyu ChenChen, Tianyu Indiana UniversityUnited States Gradual Metaprogramming
Tony ChenChen, Tony MIT A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (or: a memo on memo)
Weijun ChenChen, Weijun Shanghai Jiao Tong University, China A Programming Language for Feasible Solutions
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
Xiang ChenChen, Xiang The Hong Kong University of Science and Technology ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection
Xiangqun ChenChen, Xiangqun Peking UniversityChina Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
Yanju ChenChen, Yanju University of California, San DiegoUnited States Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-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
Zhaojun ChenChen, Zhaojun Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
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
Zhiyang ChenChen, Zhiyang University of TorontoCanada A Multi-Layer Dynamic Security Framework for DeFi Smart Contracts Session Chair of Programming Language & Compiler (part of Sponsor Invited Talks)
Baijun ChengCheng, Baijun Peking University Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
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 SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track Committee Member in Program Committee within the LMPL-track
Alvin CheungCheung, Alvin University of California at BerkeleyUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Maxime Chevalier-BoisvertChevalier-Boisvert, Maxime ShopifyCanada Committee Member in Program Committee within the MPLR-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
Shigeru ChibaChiba, Shigeru The University of TokyoJapan Steering Committee Member in Steering Committee for SPLASH 2025 Onward! Papers Co-chair in Organizing Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Session Chair of Design (part of SPLASH Onward! Papers) Co-chair in Program Committee within the SPLASH Onward! Papers-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track Committee Member in Program Committee within the MPLR-track
Zakaria ChihaniChihani, Zakaria CEA, LIST, France Verifying Neural Networks with PyRAT
Wei-Ngan ChinChin, Wei-Ngan National University of SingaporeSingapore From Delimited Continuations to Staged Logics Specifying and Verifying Future Conditions
Luca ChiodiniChiodini, Luca USI LuganoSwitzerland TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro
Shardul ChiplunkarChiplunkar, Shardul EPFLSwitzerland Practical compositional diagramming
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 Video Chair in AV Committee for ICFP/SPLASH 2025 Video Chair in Organizing Committee for ICFP/SPLASH 2025 SIGPLAN AV Report
Laurent ChristopheChristophe, Laurent Vrije Universiteit Brussel JASMaint: Portable Multi-language Taint Analysis for the Web
Ravi ChughChugh, Ravi University of Chicago Code Style Sheets: CSS for Code Committee Member in Program Committee within the HATRA-track
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
Valentin ChuravyChuravy, Valentin MIT CSAIL Committee Member in Program Committee within the PROPL-track
Luke ChurchChurch, Luke University of Cambridge \| Candela IncUnited Kingdom Organizer in Organizing Committee within the PAINT-track Committee Member in Program Committee within the PAINT-track Committee Member in Program Committee within the SPLASH Onward! Papers-track
Luisa CicoliniCicolini, Luisa University of CambridgeUnited Kingdom Interactive Bit Vector Reasoning using Verified Bitblasting
Cristina CifuentesCifuentes, Cristina Oracle Software AssuranceAustralia PC Member in Program Committee within the SPLASH Onward! Essays-track
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
Siobhán ClarkeClarke, Siobhán Trinity College Dublin, IrelandIreland Committee Member in Program Committee within the SPLASH Onward! Papers-track
Josh CluneClune, Josh Carnegie Mellon University Interactive Bit Vector Reasoning using Verified Bitblasting
Michael CoblenzCoblenz, Michael University of California, San DiegoUnited States Diversity Co-Chair in Organizing Committee for ICFP/SPLASH 2025 DEI Chair in Organizing Committee for SPLASH 2025 PC Member in Program Committee within the SPLASH Onward! Essays-track 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 Session Chair of Onward! Essays 1 (part of SPLASH Onward! Papers) A FAIR Case for a Live Computational Commons Session Chair of Session 1 (part of HATRA) Discussion Committee Member in Organizing Committee within the HATRA-track
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 Session Chair of Report, Lightning Talks, and Keynote (part of Scheme) Welcome Program Co-Chair in Organizing Committee within the Scheme-track Session Chair of I know Kung Fu (part of OlivierFest) Continuations in Music Programme Committee in Program Committee within the OlivierFest-track Committee Member in Program Committee within the PAINT-track An Interactive Learning Environment for Program Design Continuations for All: Language Design Considerations for Accessible Continuations Daisy: An Exercise Environment for Learning Information Modeling Organizing Chair in Organizing Committee within the SPLASH FARM-track Committee Member in Program Committee within the SPLASH FARM-track Types as a Specification Language for Creativity Towards an Educational Fragment of Scala
Charles ConselConsel, Charles Bordeaux-INP More than a Colleague: Celebrating Olivier’s Impact
Simon CookseyCooksey, Simon Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Nathan CoquerelCoquerel, Nathan Rennes UniversityFrance TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro
Nathan CorbynCorbyn, Nathan University of OxfordUnited Kingdom Frex: Dependently Typed Algebraic Simplification Committee Member in Program Committee within the TyDe-track
Lucas C. CordeiroCordeiro, Lucas C. University of Manchester, UKUnited Kingdom Committee Member in Program Committee within the SAS -track
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
Nathanaëlle CourantCourant, Nathanaëlle OCamlProFrance Committee Member in Program Committee within the OCaml-track
Patrick CousotCousot, Patrick Committee Member in Steering Committee within the SAS -track
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 Discussion Committee Member in Organizing Committee within the HATRA-track
Santiago CuellarCuellar, Santiago Galois, IncUnited States Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces The CoCompiler: DSL Lifting via Relational Compilation
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
Joshua DahlDahl, Joshua University of Nevada, Reno An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler
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 On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Committee Member in ICFP Programme Committee within the ICFP Papers-track
Michael DalesDales, Michael University of Cambridge, UKUnited Kingdom Programming Opportunities for the Global Biodiversity Observation Network Yirgacheffe: a declarative approach to geospatial data
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Committee Member in Program Committee within the SAS -track
Luca DanielDaniel, Luca Massachusetts Institute of Technology Lessons from Building a Hardware Compiler in Scala 3: A Practitioner Perspective
Nils Anders DanielssonDanielsson, Nils Anders University of GothenburgSweden A Formalization of Opaque Definitions for a Dependent Type Theory [Remote]
Jayanaka DantanarayanaDantanarayana, Jayanaka University of MichiganSri Lanka MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Olivier DanvyDanvy, Olivier Yale-NUS College and School of Computing, SingaporeSingapore Session Chair of Report, Lightning Talks, and Keynote (part of Scheme) Local Arrangements Chair in Organizing Committee within the Scheme-track Many Happy Continuations
Olivier DanvyDanvy, Olivier National University of SingaporeSingapore How Computer Science Was Introduced at Yale-NUS College
Olivier DanvyDanvy, Olivier Yale-NUS College and School of Computing, SingaporeSingapore Session Chair of Verification (part of SAS ) On a simple problem due to Yves Bertot
David DaraisDarais, David GaloisUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces The CoCompiler: DSL Lifting via Relational Compilation
Zaynah DargayeDargaye, Zaynah Nomadic Labs Committee Member in Program Committee within the OCaml-track
Anupam DasDas, Anupam University of Birmingham, UKUnited Kingdom Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan DaughertyDaugherty, Jonathan Galois, Inc. Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces The CoCompiler: DSL Lifting via Relational Compilation
Cristina DavidDavid, Cristina University of BristolUnited Kingdom Authoring Tools for Transparent Climate Reporting
Dylan DavisDavis, Dylan Swinburne University I Am Your Co-Pilot
Guglielmo De AngelisDe Angelis, Guglielmo CNR-IASIItaly RuntimeSave: A Graph Database of Runtime Values
Charles de Harode Haro, Charles École Normale Supérieure \| Université PSLFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Markus de Medeirosde Medeiros, Markus New York UniversityUnited States Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Wolfgang De MeuterDe Meuter, Wolfgang Vrije Universiteit BrusselBelgium Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Coen De RooverDe Roover, Coen Vrije Universiteit BrusselBelgium Steering Committee Member in Steering Committee for SPLASH 2025 Abstracting Concolic Execution for Soft Contract Verification Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Noé De SantoDe Santo, Noé University of PennsylvaniaUnited States Rebound: Efficient, expressive, and well-scoped binding
Edsko de Vriesde Vries, Edsko Well-Typed LLPNetherlands Automatic C bindings generation for Haskell
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 Committee Member in Program Committee within the LMPL-track
Konstantinos DelisDelis, Konstantinos University of Crete and FORTH-ICS SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance A Mechanized Semantics for Dataflow Circuits
Hunter DeMeyerDeMeyer, Hunter University of Illinois Urbana-Champaign Embedding WebAssembly in OCaml for Safe Program Construction
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 Quantified Underapproximation via Labeled Bunches Committee Member in ICFP Programme Committee within the ICFP Papers-track
Sam DerbyshireDerbyshire, Sam Well-Typed LLP Automatic C bindings generation for Haskell
Mehmet Oguz DerinDerin, Mehmet Oguz Unaffiliated W2GPU: Toward WebAssembly-to-WebGPU Program Translation via Small Language Models
Ankush DesaiDesai, Ankush Amazon Web ServicesUnited States Checking Observational Correctness of Database Systems Ranking Formal Specifications using LLMs
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 Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Peng DiDi, Peng Ant Group & UNSW SydneyChina Function Renaming in Reverse Engineering of Embedded Device Firmware with ChatGPT Committee Member in Program Committee within the LMPL-track
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 Steering Committee Member in Steering Committee for SPLASH 2025 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 Contract System Metatheories à la Carte: A Transition-System View of Contracts Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track The Rational Programmer, A Method for Investigating Programming Language Pragmatics
Shuo DingDing, Shuo Georgia Institute of TechnologyChina Fast Constraint Synthesis for C++ Function Templates
Alexander DingesDinges, Alexander RPTU Kaiserslautern-LandauGermany Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl) Committee Member in Program Committee within the ICFP Student Research Competition-track Binary search—think positive
Chandeepa DissanayakeDissanayake, Chandeepa Iowa State UniversityUnited States A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Purdue University Committee Member in Program Committee within the The Scala Workshop-track
Ryan DoengesDoenges, Ryan Northeastern UniversityUnited States Substructural Weakest Preconditions in Fibrations
Sébastien DoeraeneDoeraene, Sébastien EPFL, SwitzerlandSwitzerland Implementing and Evaluating a High-Level Language with WasmGC and the Wasm Component Model: Scala’s Case
Stephen DolanDolan, Stephen Jane StreetUnited Kingdom Modal Effect Types Committee Member in Program Committee within the OCaml-track Committee Member in Program Committee within the TyDe-track
Eridan DomoratskiyDomoratskiy, Eridan Saint-Petersburg State University An Empirical Study of Rational Tree Unification for miniKanren
Facundo DomínguezDomínguez, Facundo TweagUruguay Committee Member in Program Committee within the FUNARCH-track
Pablo DonatoDonato, Pablo LIX, IPP Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
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
Yuxin DongDong, Yuxin Peking University Improving SAST Detection Capability with LLMs and Enhanced DFA
Zhiqiang DongDong, Zhiqiang Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
Maximilian DoréDoré, Maximilian University of Oxford Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
Sjoerd DostDost, Sjoerd None concurrentKanren: miniKanren for parallel execution
Paul DownenDownen, Paul University of Massachusetts at LowellUnited States Session Chair of Implementation, Application, and Types (part of Scheme) Rewriting Macros on the Fly: A Modular Approach to Administrative Reduction During Expansion Controlling Copatterns: There and Back Again Programme Committee in Program Committee within the OlivierFest-track A contextual formalization of structural coinduction Committee Member in Program Committee within the TyDe-track
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 Enhancing Neural Network Robustness via Synthesis of Repair Programs
Joris DralDral, Joris Well-Typed A Layered Certifying Compiler Architecture
Steve DraperDraper, Steve University of Glasgow Let's Take Esoteric Programming Languages Seriously
Alexandre DreweryDrewery, Alexandre INRIA Contextual Equality Saturation
Derek DreyerDreyer, Derek MPI-SWSGermany JFP Announcement How to Write Papers and Give Talks that People Can Follow
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Reasoning about External Calls
Cezara DrăgoiDrăgoi, Cezara AWS / ENS Committee Member in Steering Committee within the SAS -track
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
Yalong DuDu, Yalong Harbin Institute of Technology, Shenzhen Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps
Sabhimanvi DuaDua, Sabhimanvi Swasti Precision Action Towards Climate and Health (PATCH)
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
Stéphane DucasseDucasse, Stéphane Inria; University of Lille; CNRS; Centrale Lille; CRIStALFrance Committee Member in Program Committee within the SPLASH Onward! Papers-track
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
Saikat DuttaDutta, Saikat University of Illinois at Urbana-ChampaignUnited States Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
Saikat DuttaDutta, Saikat Cornell UniversityUnited States Committee Member in Program Committee within the LMPL-track
E Harley D. Eades IIIEades III, Harley D. Augusta UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jonathan EdwardsEdwards, Jonathan IndependentUnited States Steering Committee Member in Steering Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track Committee Member in Program Committee within the HATRA-track
Attila Egri-NagyEgri-Nagy, Attila Akita International University Computational Exploration of Finite Semigroupoids
Marco EilersEilers, Marco ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Zachary EisbachEisbach, Zachary Northeastern UniversityUnited States miniDusa: An Extensible Finite-Choice Logic Programming Language (Lightning Talk)
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 A guided tour through Oxidized OCaml Session Chair of Type 2 (part of SPLASH OOPSLA) Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Taming the Flat Float Array Optimization: Tracking Separability in the Type System A Tale of Two Lambdas: A Haskeller's Journey into OCaml Career Panel
Abigail Elena ReeseElena Reese, Abigail Carnegie Mellon University Usability Barriers for Liquid Types (Summary of Published Work)
Tom EllisEllis, Tom Groq Lightning Talks Committee Member in Program Committee within the FUNARCH-track
Martin ElsmanElsman, Martin University of CopenhagenDenmark Session Chair of Applications and SRC Talks (part of ICFP Papers) Compositional Deep Argument Flattening Contractions Are Abstractions - Towards Effective Memory Management in ReML
Joel S EmerEmer, Joel S MIT/NVIDIAUnited States The Continuous Tensor Abstraction: Where Indices are Real
Burak EmirEmir, Burak Google From Facts to Theories: Deductive Databases with Mangle Datalog
Madeline EndresEndres, Madeline University of Massachusetts AmherstUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Constantin EneaEnea, Constantin LIX, CNRS, Ecole Polytechnique Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Igor EngelEngel, Igor JetBrains Research; Constructor University BremenGermany Typed Embedding of miniKanren for Functional Conversion
Sebastian ErdwegErdweg, Sebastian JGU MainzGermany Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track
Guilherme EspadaEspada, Guilherme LASIGE, University of LisbonPortugal Video Chair in AV Committee for ICFP/SPLASH 2025 SIGPLAN AV Report
Khashayar EtemadiEtemadi, Khashayar KTH Royal Institute of Technology Committee Member in Program Committee within the LMPL-track
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
Alison EyresEyres, Alison University of Cambridge Yirgacheffe: a declarative approach to geospatial data
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/SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for ICFP 2025 Student Volunteer Chair in Organizers within the ICFP/SPLASH Volunteers-track
Chris FallinFallin, Chris F5United States Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Gang FanFan, Gang Huawei Hong Kong Research CentreHong Kong SAR China Committee Member in Program Committee within the LMPL-track
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
Umar FarooqFarooq, Umar Louisiana State UniversityUnited States Web Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Products of Recursive Programs for Hypersafety Verification
Andrew FawcettFawcett, Andrew Victoria University of WellingtonNew Zealand Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities
Aleksandr FedchinFedchin, Aleksandr Tufts UniversityUnited States Metamorph: Synthesizing Large Objects from Dafny Specifications
Shon FederFeder, Shon TaridesCanada Committee Member in Program Committee within the OCaml-track
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 Committee Member in Program Committee within the MPLR-track
Joan FeigenbaumFeigenbaum, Joan Yale On Collective Control over User Interfaces in the Face of Network Eﬀects
Molly Q FeldmanFeldman, Molly Q Oberlin CollegeUnited States Committee Member in Program Committee within the HATRA-track
Frank FengFeng, Frank University of Cambridge Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings
Qiong FengFeng, Qiong Nanjing University of Science and TechnologyChina Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Xinyu FengFeng, Xinyu Nanjing University & HuaweiChina Sponsors' Message Modal Cangjie: A Preliminary Design
Yang FengFeng, Yang Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler Session Chair of Neuro-Symbolic Language/Agent Design (part of LMPL) Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study Committee Member in Program Committee within the LMPL-track
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
Daniel FerencziFerenczi, Daniel Eötvös Loránd University Evaluating AtomVM for Fault-Tolerant ESP32-Based Systems
Kiko Fernandez-ReyesFernandez-Reyes, Kiko Ericsson, SwedenSweden Session Chair of Welcome & Keynote (part of Erlang) Session Chair of Tools, Systems & Static Analysis (part of Erlang) Welcome to Erlang’25 Closing Remarks Organizing Committee in Organizing Committee within the Erlang-track
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) Generating a corpus of Hazel programs from ill-typed OCaml programs (Extended Abstract) What we talk about when we talk about scientific programming Yirgacheffe: a declarative approach to geospatial data Decomposable Type Highlighting for Bidirectional Type and Cast Systems
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
David Anthony K. FieldsFields, David Anthony K. Seton Hall University Automatic Invariant Testing for Finite-State Machines Automata Visualization for Validation and Verification: Helping Develop Correctness Arguments for Nondeterministic Machines
Andrzej FilinskiFilinski, Andrzej DIKU, University of Copenhagen More than a Colleague: Celebrating Olivier’s Impact Committee Member in ICFP Programme Committee within the ICFP Papers-track
Robert Bruce FindlerFindler, Robert Bruce Northwestern UniversityUnited States Metaprogramming in Rhombus Safe-for-Space Linked Environments Programme Committee in Program Committee within the OlivierFest-track Contract System Metatheories à la Carte: A Transition-System View of Contracts Committee Member in ICFP Programme Committee within the ICFP Papers-track A Snapshot of the Performance of Wasm Backends for Managed Languages Career Panel
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Verifying Asynchronous Hyperproperties in Reactive Systems Almost Fair Simulations
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
Kathi FislerFisler, Kathi Brown UniversityUnited States Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics
Matthew FlattFlatt, Matthew University of UtahUnited States Metaprogramming in Rhombus Safe-for-Space Linked Environments Programme Committee in Program Committee within the OlivierFest-track Session Chair of Systems (part of SPLASH OOPSLA)
Krisztian FlautnerFlautner, Krisztian University of Michigan MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Eugene FlesselleFlesselle, Eugene EPFLSwitzerland Capability-Safe Erasure in Scala
Matthew FluetFluet, Matthew Rochester Institute of TechnologyUnited States Committee Member in Program Committee within the Haskell-track
Cyril Flurin MoserFlurin Moser, Cyril ETH Zurich Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Olivier FlückigerFlückiger, Olivier GoogleSwitzerland Committee Member in Program Committee within the VMIL-track
Arsenii FominFomin, Arsenii Eötvös Loránd University Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Mechanised Proofs of Atom Exhaustion in Erlang
Alcides FonsecaFonseca, Alcides LASIGE; University of LisbonPortugal ROSpec: A Domain-Specific Language for ROS-based Robot Software Usability Barriers for Liquid Types (Summary of Published Work)
Darius FooFoo, Darius National University of Singapore From Delimited Continuations to Staged Logics Specifying and Verifying Future Conditions Committee Member in Program Committee within the OCaml-track
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
Björn FrankeFranke, Björn University of EdinburghUnited Kingdom Committee Member in Program Committee within the MPLR-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
Yuxi FuFu, Yuxi Shanghai Jiao Tong University, China A Programming Language for Feasible Solutions
Maika FujiiFujii, Maika Ochanomizu University Defining Algebraic Effects and Handlers via Trails and Metacontinuations
Juan FumeroFumero, Juan OracleItaly Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Viktória FördősFördős, Viktória Cisco SystemsSweden Committee Member in Program Committee within the Erlang-track
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
Zeinab GalalGalal, Zeinab University of Bologna Committee Member in Program Committee within the HOPE-track
Catarina GamboaGamboa, Catarina Carnegie Mellon University and University of LisbonPortugal Usability Barriers for Liquid Types (Summary of Published Work)
Emma GandonouGandonou, Emma Pomona College [CANCELED] Adaptive Search Synthesis as a Recursion Scheme
Pierre GantyGanty, Pierre IMDEA Software Institute, Spain Committee Member in Program Committee within the SAS -track
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
Zac GarbyGarby, Zac University of NottinghamUnited Kingdom The Calculated Typer (Functional Pearl)
Andrés M. GarcedGarced, Andrés M. Seton Hall University Automatic Invariant Testing for Finite-State Machines 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 Career Panel Verified Software at Scale
Deepak GargGarg, Deepak MPI-SWSGermany Non-interference Preserving Optimising Compilation Fusing Session-Typed Concurrent Programming into Functional Programming Committee Member in ICFP Programme Committee within the ICFP Papers-track
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
Matthew GaudetGaudet, Matthew MozillaCanada Committee Member in Program Committee within the MPLR-track
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 GellerGeller, Adam Computer Science, University of British ColumbiaCanada Type-Preserving Flat Closure Optimization
Samir GenaimGenaim, Samir Universidad Complutense de MadridSpain Committee Member in Program Committee within the SAS -track
Eve GengGeng, Eve Chalmers University of Technology, Gothenburg, Sweden A Formalization of Opaque Definitions for a Dependent Type Theory [Remote]
Jared GentnerGentner, Jared None How to Score in the Art Racket
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 Session Chair of Algorithms (part of ICFP Papers) Call-Guarded Abstract Definitional Interpreters SRC Awards Student Research Competition Chair in Program Committee within the ICFP Student Research Competition-track
Jad Elkhaleq GhalayiniGhalayini, Jad Elkhaleq University of CambridgeUnited Kingdom Sound and Complete Refinement for SSA with Substructural Effects
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
Roberto GiacobazziGiacobazzi, Roberto University of ArizonaUnited States Committee Member in Steering Committee within the SAS -track
Ryan GibbGibb, Ryan University of Cambridge Functional Networking for Millions of Docker Desktops (Experience Report) Three steps for OCaml to crest the AI humps Spatial Programming for Environmental Monitoring
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
Elena GlassmanGlassman, Elena Harvard UniversityUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Nathan GloverGlover, Nathan Carnegie Mellon University Integrating Resource Analyses via Resource Decomposition
Robert GlückGlück, Robert University of CopenhagenDenmark Committee Member in Program Committee within the Scheme-track Redundancy Checking in Reversible Flowcharts via Logic-Based Operational Semantics Programme Committee in Program Committee within the OlivierFest-track
Brighten GodfreyGodfrey, Brighten UIUC and Broadcom SafeTree: Expressive Tree Policies for Microservices
Muluh GodsonGodson, Muluh Tarides A New Era of OCaml Editing: Powered by Merlin, Delivered via LSP
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
Elisa Gonzalez BoixGonzalez Boix, Elisa Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the SPLASH Onward! Papers-track BabelBridge: A Control-Flow Graph Debugger for Microcontrollers Dynamic Analysis Extending a Shadow Runtime for Profit JASMaint: Portable Multi-language Taint Analysis for the Web A Control-Flow Graph Approach to Language-Agnostic Debugging for Microcontrollers
Andrew GonzalezGonzalez, Andrew McGill University Programming Opportunities for the Global Biodiversity Observation Network
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 Committee Member in Program Committee within the ML Family Workshop-track Co-chair in Program Committee within the OCaml-track
Colin GordonGordon, Colin Drexel UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025 Onward! Essays Co-chair in Organizing Committee for SPLASH 2025 Program Chair in Program Committee within the SPLASH Onward! Essays-track Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Modal Abstractions for Virtualizing Memory Addresses Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Roberta GoriGori, Roberta Diaprtimento di Informatica, Universita' di Pisa, Italy Revealing Sources of (Memory) Errors via Backward Analysis
Daniel GorinGorin, Daniel Meta Session Chair of Formal Semantics & Verification (part of Erlang) A stop-the-world debugger for Erlang (and the BEAM)
Jérôme GorinGorin, Jérôme GeNumErFrance On Dynamic Multimedia Pipelines for Opening Browsers to New Formats
Alessandra GorlaGorla, Alessandra IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Chester GouldGould, Chester University of British Columbia Type-Preserving Flat Closure Optimization Towards a Performance Comparison of Syntax and Type-Directed NbE (Extended Abstract)
Hemant GouniGouni, Hemant Carnegie Mellon UniversityUnited States Structural Information Flow: A Fresh Look at Types for Non-Interference Session Chair of Type systems 1 (part of IWACO) Session Chair of Type systems 2 (part of IWACO) Round table on ownership challenges Committee Member in Organizing Committee within the IWACO-track
Pierre GoutagnyGoutagny, Pierre Inria and University of LilleFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
John GouwarGouwar, John Northeastern UniversityUnited States Scaling Optimization Over Uncertainty via Compilation
Kevin GraafGraaf, Kevin Independent Researcher Carving Text at Its Joints: A New Perspective on Writing and Computers
Fernanda GraciolliGraciolli, Fernanda Midspiral The Modular Imperative: Rethinking LLMs for Maintainable Software
Marcos GranduryGrandury, Marcos IMDEA Software Institute; Universidad Politécnica de MadridSpain Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
Maksim GrankinGrankin, Maksim BloombergUnited Kingdom Toward a More Secure OCaml Ecosystem
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/SPLASH 2025 Workshops Co-Chair in Organizing Committee for ICFP 2025 Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track
Ben GreenmanGreenman, Ben University of UtahUnited States Committee Member in Program Committee within the Scheme-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Ben GreenmanGreenman, Ben University of Utah, USA Committee Member in Program Committee within the HATRA-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
Rudi GrinbergGrinberg, Rudi OCaml Labs OCaml Package Management with (only!) Dune
Charlène GrosGros, Charlène ISEN Lille Committee Member in Program Committee within the OCaml-track
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
Adam GundryGundry, Adam Well-Typed LLPUnited Kingdom Committee Member in Program Committee within the Haskell-track
Xiangyu GuoGuo, Xiangyu Arizona State University Encoding Numeric Computations and Infusing Heuristic Knowledge Using Integrity Constraints in stableKanren
Yao GuoGuo, Yao Peking UniversityChina Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
Aarti GuptaGupta, Aarti Princeton University Ranking Formal Specifications using LLMs
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 Organizing Committee for SPLASH 2025 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track OOPSLA Artifact Awards
Björn GustavssonGustavsson, Björn Ericsson AB A stop-the-world debugger for Erlang (and the BEAM)
Claudio GutierrezGutierrez, Claudio DCC, Universidad de Chile & IMFD Flexible and Expressive Typed Path Patterns for GQL
Ulysse GérardGérard, Ulysse Tarides A New Era of OCaml Editing: Powered by Merlin, Delivered via LSP
Matthias GüdemannGüdemann, Matthias University of Applied Sciences MunichGermany Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
H Huong HaHa, Huong RMIT UniversityAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
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 Debugging for Scala Control Flow DSLs
Hamed HaddadiHaddadi, Hamed Imperial College London Spatial Programming for Environmental Monitoring
Kerry HaganHagan, Kerry University of Illinois, Urbana-ChampaignUnited States Cellular Automata as a Model For 1-bit Synthesis in Mitosis Concert: Mitosis
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom The Power of Regular Constraint Propagation
Ákos HajduHajdu, Ákos MetaUnited Kingdom Welcome to Erlang’25
Ákos HajduHajdu, Ákos MetaUnited Kingdom Closing Remarks Organizing Committee in Organizing Committee within the Erlang-track
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
Philipp HallerHaller, Philipp KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the SPLASH Onward! Papers-track
Stefan HallerstedeHallerstede, Stefan Aarhus University Danvy’s Mystery Functions in Slang
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
Li HaoyiHaoyi, Li IndependentSingapore Simpler Scala Builds with Functional and Object-Oriented Programming
Umut Sarp HarbaliogluHarbalioglu, Umut Sarp The University of Manchester Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware
Ben HardekopfHardekopf, Ben University of California at Santa BarbaraUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Adi HarifHarif, Adi Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
Frederick C. Harris Jr.Harris Jr., Frederick C. University of Nevada, RenoUnited States An Argument for the Practicality of Entity Component Systems as the Primary Data Structure for an Interpreter or Compiler
Tim HarrisHarris, Tim OpenAIUnited Kingdom Committee Member in Program Committee within the MPLR-track
Paul HarveyHarvey, Paul University of Glasgow, UK Committee Member in Program Committee within the Erlang-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
John HatcliffHatcliff, John Kansas State University Danvy’s Mystery Functions in Slang Programme Committee in Program Committee within the OlivierFest-track
Matthias HauswirthHauswirth, Matthias USI LuganoSwitzerland TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro 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
Deyuan (Mike) HeHe, Deyuan (Mike) Princeton UniversityUnited States Ranking Formal Specifications using LLMs
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
Jingxuan HeHe, Jingxuan University of California at BerkeleyUnited States Committee Member in Program Committee within the LMPL-track
Jingzhu HeHe, Jingzhu ShanghaiTech UniversityChina Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-Procedural Path-Sensitive Taint Analysis
Ningyu HeHe, Ningyu Hong Kong Polytechnic UniversityHong Kong SAR China Committee Member in Program Committee within the SAS -track
Pinjia HeHe, Pinjia Chinese University of Hong Kong, ShenzhenChina Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Program Committee within the LMPL-track
Qi HeHe, Qi Nanjing University Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study
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
Xuehuai HeHe, Xuehuai Yale University [CANCELED] Adaptive Search Synthesis as a Recursion Scheme
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
Dasari Gnana HeemmanshuuHeemmanshuu, Dasari Gnana Indian Institute of Technology Bombay ScalaF: Functional Refactoring Suggestions for Scala
Maxwell HeiberHeiber, Maxwell MetaUnited Kingdom The State of The Unions: challenges for type-checking unions and generics at WhatsApp
Nicole HeinimannHeinimann, Nicole Technische Universität BerlinGermany Video Chair in AV Committee for ICFP/SPLASH 2025 Video Chair in Organizing Committee for ICFP/SPLASH 2025
Sonja HeinzeHeinze, Sonja TaridesSpain A New Era of OCaml Editing: Powered by Merlin, Delivered via LSP
Jason HemannHemann, Jason Seton Hall UniversityUnited States Session Chair of Relational conversion, compilation, and encoding (part of miniKanren) Frontiers: What's next for miniKanren and Relational Programming? Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics Publicity Chair in Organizing Committee within the miniKanren-track
Fritz HengleinHenglein, Fritz University of CopenhagenDenmark Committee Member in Distinguished Papers Committee for ICFP 2025 Opening Simple Closure Analysis Revisited Organizer in Program Committee within the OlivierFest-track 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 SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025 Programme Committee in Program Committee within the OlivierFest-track SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Kihong HeoHeo, Kihong KAISTSouth Korea Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Felienne HermansHermans, Felienne Vrije Universiteit AmsterdamNetherlands SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025 SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track
Manuel HermenegildoHermenegildo, Manuel Technical University of Madrid (UPM) and IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Brandon HewerHewer, Brandon University of Nottingham Committee Member in Program Committee within the TyDe-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 Committee Member in Program Committee within the Scheme-track Modal Effect Types
Ralf HinzeHinze, Ralf RPTU Kaiserslautern-Landau Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
Ralf HinzeHinze, Ralf RPTU Kaiserslautern-LandauGermany Binary search—think positive
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism Session Chair of Concurrency (part of ICFP Papers)
Robert HirschfeldHirschfeld, Robert Hasso Plattner Institute; University of PotsdamGermany Steering Committee Member in Steering Committee for SPLASH 2025 Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions Block-based Editing in a Textual World Organizer in Organizing Committee within the PAINT-track Committee Member in Program Committee within the PAINT-track Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
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 Committee Member in Program Committee within the OCaml-track
Csaba HochHoch, Csaba Cursor InsightHungary Committee Member in Program Committee within the Erlang-track
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Integrating Resource Analyses via Resource Decomposition Committee Member in ICFP Programme Committee within the ICFP Papers-track
Daniel HolleHolle, Daniel Baden-Wuerttemberg Cooperative State University Heterogeneous translation of Scala-like function types in Java-TX
Reid HolmesHolmes, Reid University of British ColumbiaCanada Committee Member in Program Committee within the SPLASH Onward! Papers-track 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
Michael HomerHomer, Michael Victoria University of WellingtonNew Zealand Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities Fast & Easy ASTs for Flexible Embedded Interpreters
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
Hongwei XiHongwei Xi Boston University Committee Member in Program Committee within the TyDe-track
Dániel HorpácsiHorpácsi, Dániel Eötvös Loránd UniversityHungary Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Mechanised Proofs of Atom Exhaustion in Erlang Committee Member in Program Committee within the Erlang-track
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) Session Chair of MPLR Keynote & Research Paper 2 (part of MPLR) Committee Member in Program Committee within the MPLR-track
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 Committee Member in Program Committee within the HOPE-track Committee Member in Program Committee within the PROPL-track
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 Associate Chair in OOPSLA Review Committee within the SPLASH OOPSLA-track Effectful Lenses: There and Back with Different Monads Compositions for Free: Reasoning about Effectful Lenses
Heqing HuangHuang, Heqing City University of Hong Kong Publicity Co-Chair, Web Co-Chair in Organizing Committee for SPLASH 2025
Isabell HuangHuang, Isabell Committee Member in Program Committee within the Erlang-track
Jeff HuangHuang, Jeff Texas A&M UniversityUnited States Workshops Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Workshop Co-Chair in Organizing Committee for SPLASH 2025 Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
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 (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging Liberating Merges via Apartness and Guarded Subtyping Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Yulong HuangHuang, Yulong University of CambridgeUnited Kingdom TEAL: a Total Expressive Assembly Language
Zixin HuangHuang, Zixin University of Illinois at Urbana-Champaign, USA Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
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
Graham HuttonHutton, Graham University of NottinghamUnited Kingdom The Calculated Typer (Functional Pearl)
Doha HwangHwang, Doha Samsung PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Brian Hyeongseok KimHyeongseok Kim, Brian University of Southern California Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
I Ruxandra IcleanuIcleanu, Ruxandra University of Edinburgh SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F
Roberto IerusalimschyIerusalimschy, Roberto PUC-RioBrazil Committee Member in Program Committee within the MPLR-track
Yuka IkarashiIkarashi, Yuka Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Mirai IkebuchiIkebuchi, Mirai Kyoto UniversityJapan Committee Member in Program Committee within the ML Family Workshop-track
Kazuki IkemoriIkemori, Kazuki Tokyo Institute of Technology Continuations for All: Language Design Considerations for Accessible Continuations
Danko IlikIlik, Danko Trusted LabsFrance From continuation models to shift without reset and an intuitionistic arithmetical hierarchy
Keigo ImaiImai, Keigo DeNA Co., Ltd.Japan Committee Member in Program Committee within the ML Family Workshop-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Video Chair in AV Committee for ICFP/SPLASH 2025
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
Shachar ItzhakyItzhaky, Shachar TechnionIsrael Ductape: Optimizing Dynamically Typed Programs using Ahead-of-Time Compilation and Data-Flow Analysis
Hideya IwasakiIwasaki, Hideya Meiji University Committee Member in Program Committee within the Haskell-track
Maliheh IzadiIzadi, Maliheh Delft University of TechnologyNetherlands Committee Member in Program Committee within the LMPL-track
Yusuke IzawaIzawa, Yusuke Tokyo Metropolitan UniversityJapan Session Chair of Keynote / Language Semantics & Type Systems (part of VMIL) Closing Welcome Co-chair in Program Committee within the VMIL-track Co-chair in Organizing Committee within the VMIL-track Committee Member in Program Committee within the PAINT-track
J Guilhem JaberJaber, Guilhem Nantes UniversitéFrance Co-chair in Program Committee within the HOPE-track
Daniel JacksonJackson, Daniel MIT What You See Is What It Does: A Structural Pattern for Legible Software
Jules JacobsJacobs, Jules Jane StreetUnited States Web Co-Chair in Organizing Committee for ICFP/SPLASH 2025 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
Sadiq JafferJaffer, Sadiq University of CambridgeUnited Kingdom Three steps for OCaml to crest the AI humps Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings
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 End-to-End Compiler Infrastructure for Emerging Tensor Accelerators SPLAT: A framework for optimised GPU code-generation for SParse reguLar ATtention
Joel JakubovicJakubovic, Joel Charles University in PragueCzechia [Invited Talk] Notational Freedom via Self-Raising Diagrams The Unix Executable as a Smalltalk Method Committee Member in Program Committee within the SPLASH Onward! Papers-track
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
Sujin JangJang, Sujin KAISTSouth Korea Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Thomas P. JensenJensen, Thomas P. INRIA Rennes Contextual Equality Saturation
Minseok JeonJeon, Minseok DGISTSouth Korea PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns Committee Member in ICFP Programme Committee within the ICFP Papers-track
Mingyeong JeongJeong, Mingyeong Chungnam National University Type Checking for Python Using Intersection Types
Seokhun JeongJeong, Seokhun KAIST P4-SpecTec: A Language Mechanization Framework for P4
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 Freezing Bidirectional Typing (Extended Abstract)
Yu JiangJiang, Yu Tsinghua UniversityChina Function Renaming in Reverse Engineering of Embedded Device Firmware with ChatGPT Committee Member in Program Committee within the LMPL-track
Yuchao JiangJiang, Yuchao UNSWAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Yuchen JiangJiang, Yuchen University of MichiganUnited States Notions of Stack-manipulating Computation and Relative Monads
Abhilash JindalJindal, Abhilash IIT Delhi, IndiaIndia STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management GPU-accelerated Hydrology Algorithms for On-prem Computation: Flow accumulation, Drainage lines, Watershed delineation, Runoff simulation
Vatsal JingarJingar, Vatsal IIT Delhi GPU-accelerated Hydrology Algorithms for On-prem Computation: Flow accumulation, Drainage lines, Watershed delineation, Runoff simulation
Mingyu JoJo, Mingyu Korea University Lemma Discovery for Inductive Equational Proofs via Recursive Function Synthesis
Patricia JohannJohann, Patricia Appalachian State University Committee Member in Program Committee within the Haskell-track
Jacob JohannsenJohannsen, Jacob IndependentDenmark More than a Colleague: Celebrating Olivier’s Impact
Iris JohnsonJohnson, Iris NHL Stenden University of Applied SciencesNetherlands Committee Member in Program Committee within the SPLASH FARM-track
Sarah JohnsonJohnson, Sarah Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Michael Peyton JonesJones, Michael Peyton Input Output, United Kingdom Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Saurabh JoshiJoshi, Saurabh Indian Institute Of Technology Delhi STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management
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
Dipesh KafleKafle, Dipesh NIT Trichy, Tiruchirappalli, India A Mechanically Verified Garbage Collector for OCaml
Gowtham KakiKaki, Gowtham University of Colorado at BoulderUnited States Bolt-On Strong Consistency: Specification, Implementation, and Verification
Diana KalinichenkoKalinichenko, Diana Jane Street Taming the Flat Float Array Optimization: Tracking Separability in the Type System
Antanas KalkauskasKalkauskas, Antanas Nanyang Technological University Updating WasmCert-Isabelle to WebAssembly 2.0
Sanne KalkmanKalkman, Sanne CodeSandbox \| TogetherAINetherlands Committee Member in Program Committee within the Erlang-track
Konstantinos KallasKallas, Konstantinos University of California, Los AngelesUnited States Opportunistically Parallel Lambda Calculus
Kannupriya KalraKalra, Kannupriya SKY HQ, LondonUnited Kingdom Mentoring in the Scala Ecosystem: Insights from Google Summer of Code
Shoaib KamilKamil, Shoaib Adobe Research Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Arsyad KamiliKamili, Arsyad Singapore A Concurrency-Testing Approach for Detecting Isolation Level Bugs in Database Systems
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
Matthew KaneyKaney, Matthew Weft—Enabling Tidal on the Web
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
Jerzy KarczmarczukKarczmarczuk, Jerzy University of CaenFrance Functional Programming and Computational Quantum Structures
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
Jamie M. KassKass, Jamie M. Tohoko University Programming Opportunities for the Global Biodiversity Observation Network
Jun KatoKato, Jun National Institute of Advanced Industrial Science and Technology (AIST)Japan Committee Member in Program Committee within the SPLASH Onward! Papers-track
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Hiroyuki KatsuraKatsura, Hiroyuki University of Cambridge Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Tomer KatzKatz, Tomer Technion Israel Institute of Technology ScooPy: Enhancing Program Synthesis with Nested Example Specifications
Ryan KavanaghKavanagh, Ryan Université du Québec à MontréalCanada Fusing Session-Typed Concurrent Programming into Functional Programming Committee Member in Program Committee within the ICFP Student Research Competition-track
Alex KavvosKavvos, Alex University of BristolUnited Kingdom Adequacy for Algebraic Effects Revisited Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Session Chair of Denotational Semantics (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track
Alex KeizerKeizer, Alex University of Cambridge Interactive Bit Vector Reasoning using Verified Bitblasting
Stephen KellKell, Stephen King's College LondonUnited Kingdom Steering Committee Member in Steering Committee for SPLASH 2025 Session Chair of Compilation Techniques (part of VMIL) Committee Member in Program Committee within the VMIL-track Steering Committee Chair in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Session Chair of Onward! Papers and Essay (part of SPLASH Onward! Papers) Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track Committee Member in Program Committee within the MPLR-track
Chantal KellerKeller, Chantal LMF - University Paris-SaclayFrance Towards Metaprogramming Defunctionalization in Rocq More than a Colleague: Celebrating Olivier’s Impact Programme Committee in Program Committee within the OlivierFest-track
Gabriele KellerKeller, Gabriele Utrecht UniversityNetherlands A Layered Certifying Compiler Architecture
Martin KelloggKellogg, Martin New Jersey Institute of TechnologyUnited States Sponsorship Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Sponsorship Co-Chair in Organizing Committee for SPLASH 2025 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
Srinivasan KeshavKeshav, Srinivasan University of Cambridge Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings
Harun KhanKhan, Harun Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Raffi KhatchadourianKhatchadourian, Raffi CUNY Hunter CollegeUnited States Committee Member in Program Committee within the VMIL-track Committee Member in Program Committee within the SPLASH Onward! Papers-track
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
Roman KireevKireev, Roman Input Output, United Kingdom Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Marisa KirisameKirisame, Marisa University of UtahUnited States Incremental Bidirectional Typing via Order Maintenance
Oleg KiselyovKiselyov, Oleg Tohoku UniversityJapan A Pair of tricks Programme Committee in Program Committee within the OlivierFest-track
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
Samuel KlumpersKlumpers, Samuel KU Leuven, Belgium Staging Automatic Differentiation with Fusion
Edward KmettKmett, Edward Positron AIUnited States Committee Member in Program Committee within the miniKanren-track
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia SinicaTaiwan Committee Member in Program Committee within the Haskell-track
Naoki KobayashiKobayashi, Naoki University of TokyoJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Mark KochKoch, Mark Quantinuum Fulls Seldom Differ
Matěj KocourekKocourek, Matěj Charles UniversityCzechia Copy-and-Patch Just-in-Time Compiler for R
Maximilian KodetzkiKodetzki, Maximilian Karlsruhe Institute of TechnologyGermany X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Wen KokkeKokke, Wen Well-TypedUnited Kingdom Committee Member in Program Committee within the TyDe-track
Takashi KokubunKokubun, Takashi ShopifyUnited States ZJIT: Building a New JIT Compiler for Ruby
John C. KolesarKolesar, John C. Yale UniversityUnited States Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Iacovos KolokasisKolokasis, Iacovos University of Crete and FORTH-ICSGreece Session Chair of Runtime Systems & Tooling (part of VMIL) MaTSa: Race Detection in Java Committee Member in Program Committee within the VMIL-track SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Proof-Carrying Neuro-Symbolic Code
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Session Chair of Macros and Denotational Semantics (part of Scheme) Committee Member in Program Committee within the Scheme-track Type-Preserving Flat Closure Optimization Type Universes as Kripke Worlds Type Universes as Kripke Worlds: Memory Management Edition Graduate Student Panel How to Get the Most Out of a Conference
Dmitrii KosarevKosarev, Dmitrii An Empirical Study of Rational Tree Unification for miniKanren
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
Daisuke KotaniKotani, Daisuke Kyoto University Bringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly Programs
Christos KotselidisKotselidis, Christos University of Manchester/Nimble InnovationUnited Kingdom Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Nikita KovalKoval, Nikita JetBrainsNetherlands Concurrent Algorithms under the hood of Kotlin Coroutines Testing concurrent code on JVM with Lincheck Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
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 Committee Member in Organising Committee within the TyDe-track Committee Member in Program Committee within the Haskell-track
Laura KovácsKovács, Laura TU WienAustria Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Gintas KraptavičiusKraptavičius, Gintas Concert: Merzmania
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya Harvard UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track The Modular Imperative: Rethinking LLMs for Maintainable Software
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
Maks KretKret, Maks The University of Edinburgh ScaIR: Type-safe Compiler Framework Compatible with MLIR
Jacco KrijnenKrijnen, Jacco Utrecht UniversityNetherlands A Tale of Two Zippers A Layered Certifying Compiler Architecture
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 Committee Member in Program Committee within the MPLR-track
Shriram KrishnamurthiKrishnamurthi, Shriram Brown UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025 OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025 A guided tour through Oxidized OCaml 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 Sharing is Scaring: Linking Cloud File-Sharing to Programming Language Semantics Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Sound and Complete Refinement for SSA with Substructural Effects
Paul KrogmeierKrogmeier, Paul University of Illinois at Urbana-ChampaignUnited States Synthesizing DSLs for Few-Shot Learning
Marek KubicaKubica, Marek Tarides OCaml Package Management with (only!) Dune
Nikolai KudasovKudasov, Nikolai Innopolis UniversityRussia typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell
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
rahul kumarkumar, rahul GPU-accelerated Hydrology Algorithms for On-prem Computation: Flow accumulation, Drainage lines, Watershed delineation, Runoff simulation
Lindsey KuperKuper, Lindsey University of California, Santa CruzUnited States Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track CRDT Emulation, Simulation, and Representation Independence Freer Arrows and Why You Need Them in Haskell
Ivan KurajKuraj, Ivan Massachusetts Institute of Technology Peepco: Batch-Based Consistency Optimization
Ismail KuruKuru, Ismail Drexel UniversityUnited States Modal Abstractions for Virtualizing Memory Addresses
Kira KutscherKutscher, Kira More than a Colleague: Celebrating Olivier’s Impact
Christian KästnerKästner, Christian Carnegie Mellon University Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Filip KřikavaKřikava, Filip Czech Technical University in PragueCzechia Rebase Chair in Organizing Committee for SPLASH 2025 Copy-and-Patch Just-in-Time Compiler for R Session Chair of REBASE (part of REBASE) Session Chair of REBASE (part of REBASE) Session Chair of REBASE (part of REBASE) Committee Member in Organizing Committee within the REBASE-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
Patrick LamLam, Patrick University of Waterloo Committee Member in Program Committee within the SPLASH Onward! Papers-track
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
Yingjun LanLan, Yingjun Formal Verification of Graham's Scan Algorithm
Jens Kanstrup LarsenLarsen, Jens Kanstrup DTUDenmark Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Pascal LasnierLasnier, Pascal University of Cambridge Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk)
Saharsh LaudLaud, Saharsh Indian Institute Of Technology DelhiIndia STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management
Jacob LaurelLaurel, Jacob Georgia Institute of TechnologyUnited States Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
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 Session Chair of Closure (part of OlivierFest) Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core Opening Organizer in Program Committee within the OlivierFest-track 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
Tristan Le GallLe Gall, Tristan CEA LIST Verifying Neural Networks with PyRAT
Claire Le GouesLe Goues, Claire Carnegie Mellon University Committee Member in Organizing Committee within the LMPL-track
Justin LeLe, Justin Machine Learning Primitives as Algebraic Effects Four Years of Embedded Haskell in Critical Real-Time Systems: Lessons and Insights
Quang Loc LeLe, Quang Loc University College LondonUnited Kingdom Committee Member in Program Committee within the SAS -track
Van-Hoang LeLe, Van-Hoang The University of NewcastleAustralia Committee Member in Review Committee within the SPLASH Student Research Competition-track
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 Taking away Mutation Committee Member in Program Committee within the The Scala Workshop-track
HYEONJIN LEELEE, HYEONJIN On A Multitier Actor Programming Language
Jaehyun LeeLee, Jaehyun KAISTSouth Korea P4-SpecTec: A Language Mechanization Framework for P4
Jaeseo LeeLee, Jaeseo POSTECHSouth Korea Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
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
Wonyeol LeeLee, Wonyeol POSTECHSouth Korea On the Structure of Abstract Interpreters
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/SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for ICFP 2025 Student Volunteer Chair in Organizers within the ICFP/SPLASH Volunteers-track
Zheng Han LeeLee, Zheng Han National University of Singapore, Singapore Efficient Decrease-And-Conquer Linearizability Monitoring
Yanni LefkiLefki, Yanni InriaFrance A Core Language for Extended Pattern Matching and Binding Boolean Expressions
Paul LegerLeger, Paul Universidad Católica del Norte, ChileChile Committee Member in Program Committee within the VMIL-track
Maxime LegoupilLegoupil, Maxime Aarhus University Iris-Wasm: reasoning formally about Wasm and Wasm extensions
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
Julien LehmannLehmann, Julien CEA, LIST, FranceFrance Verifying Neural Networks with PyRAT
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track First-Order Laziness Career Panel
Matthieu LemerreLemerre, Matthieu Université Paris-Saclay - CEA ListFrance On the Structure of Abstract Interpreters Programme Committee in Program Committee within the OlivierFest-track
Augustin LemesleLemesle, Augustin CEA, LIST, France Verifying Neural Networks with PyRAT
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
David LeopoldsederLeopoldseder, David Oracle LabsAustria Committee Member in Program Committee within the MPLR-track
Sorin LernerLerner, Sorin University of California at San DiegoUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-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
Danya LetteLette, Danya Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-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 Flix: A Design for Language-Integrated Datalog Qualified Types with Boolean Algebras A simple blame calculus for explicit nulls Taking away Mutation
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 Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
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
Haokun LiLi, Haokun Peking University Preguss: It Analyzes, It Specifies, It Verifies
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 Substructural Weakest Preconditions in Fibrations
Juanen LiLi, Juanen Beijing Normal University Structural Abstraction and Refinement for Probabilistic Programs
Kwing Hei LiLi, Kwing Hei Aarhus UniversityDenmark Separation Logics for Probability, Concurrency, and Security 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 Embedding Quantum Program Verification into Dafny A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
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
Paley LiLi, Paley Oracle Fast and Compact: Reducing Size of AOT-Compiled Java Code Without Sacrificing Performance
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 Committee Member in Program Committee within the LMPL-track
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
Yao LiLi, Yao Portland State UniversityUnited States A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants Committee Member in Program Committee within the TyDe-track Freer Arrows and Why You Need Them in Haskell
Yi LiLi, Yi Nanyang Technological UniversitySingapore TailTracer: Continuous Tail Tracing for Production Use Committee Member in Program Committee within the LMPL-track
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 Co-chair in SAS Artifact Evaluation Committee within the SAS Artifact-track
Yuze LiLi, Yuze Virginia TechUnited States Memory Tiering in Python Virtual Machine
Zhong LiLi, Zhong Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Ziyang LiLi, Ziyang Johns Hopkins UniversityUnited States Committee Member in Program Committee within the LMPL-track
Zongjie LiLi, Zongjie The Hong Kong University of Science and Technology Reasoning as a Resource: Optimizing Fast and Slow Thinking in Code Generation Models
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
Slim LimLim, Slim UC Berkeley, Notion LabsUnited States Committee Member in Program Committee within the HATRA-track
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
Tengjie LinLin, Tengjie Zhejiang University Preguss: It Analyzes, It Specifies, It Verifies
Youfang LinLin, Youfang Beijing Jiaotong University Fuzzing C++ Compilers via Type-Driven Mutation
Jens LinckeLincke, Jens Hasso Plattner Institute; University of PotsdamGermany Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom ICFP'23 Program Chair in Steering Committee for ICFP 2025 Session Chair of Continuations at Work (part of OlivierFest) Encoding Product Types Programme Committee in Program Committee within the OlivierFest-track Modal Effect Types First-Order Laziness Freezing Bidirectional Typing (Extended Abstract) Committee Member in Program Committee within the WebAssembly Workshop-track Rows and Capabilities as Modal Effects (Extended Abstract)
Yuxi LingLing, Yuxi National University of Singapore Graduate Student Panel
Benjamin LionLion, Benjamin INRIA Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Teodors LisovenkoLisovenko, Teodors Ca' Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Kyle LittleLittle, Kyle University of Utah SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Amanda LiuLiu, Amanda Massachusetts Institute of TechnologyUnited States Gauguin, Descartes, Bayes: A Diurnal Golem's Brain
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
Hongyu LiuLiu, Hongyu Huawei ChinaChina Committee Member in Program Committee within the LMPL-track Session Chair of Program Analysis & Testing (part of Sponsor Invited Talks)
Jie LiuLiu, Jie ByteDanceChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Puzhuo LiuLiu, Puzhuo Ant Group & Tsinghua UniversityChina Session Chair of LLMs for Program Analysis and Verification I (part of LMPL) Function Renaming in Reverse Engineering of Embedded Device Firmware with ChatGPT
Rocky LiuLiu, Rocky MetaUnited States Gradual Metaprogramming
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
Yang LiuLiu, Yang Nanyang Technological UniversitySingapore [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track
Yepang LiuLiu, Yepang Southern University of Science and TechnologyChina Committee Member in Program Committee within the LMPL-track
Yue LiuLiu, Yue Data61, CSIRO Committee Member in Review Committee within the SPLASH Student Research Competition-track
Zixi LiuLiu, Zixi Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler
Ziyang LiuLiu, Ziyang Input Output, USA Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
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
Steven LolongLolong, Steven University of TübingenGermany The MNL: A Block-based Functional Programming Language with Reactive Blocks
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
Huan LongLong, Huan Shanghai Jiao Tong University A Programming Language for Feasible Solutions
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
Jean-Michel LordLord, Jean-Michel McGill University Programming Opportunities for the Global Biodiversity Observation Network
Anton LorenzenLorenzen, Anton University of EdinburghUnited Kingdom Modal Effect Types First-Order Laziness Session Chair of ML Workshop 3 (part of ML Family Workshop) Committee Member in Program Committee within the ML Family Workshop-track Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad Graduate Student Panel
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
Yiling LouLou, Yiling Fudan UniversityChina Committee Member in Program Committee within the LMPL-track
Jean-Pierre LoziLozi, Jean-Pierre InriaFrance Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core
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
Justin LubinLubin, Justin University of California at BerkeleyUnited States Committee Member in Program Committee within the HATRA-track
Jonathan LudlamLudlam, Jonathan University of Cambridge Three steps for OCaml to crest the AI humps
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
Yuan LuoLuo, Yuan Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
Matthew LutzeLutze, Matthew Aarhus University The Simple Essence of Monomorphization Type-safe Blazon - Enforcing Pedantry in Heraldic Design
Pedro López-GarcíaLópez-García, Pedro IMDEA Software Institute Committee Member in Program Committee within the SAS -track
Júnior LöffLöff, Júnior Università della Svizzera italiana HeapBuffers: Why not just using a binary serialization format for your managed memory?
Andres LöhLöh, Andres Well-Typed LLPUnited Kingdom Committee Member in Program Committee within the Haskell-track
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 Lexical Effect Handler: Fast by Design, Correct by Proof 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
Weixi MaMa, Weixi MetaUnited States Gradual Metaprogramming
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
Kenneth MacKenzieMacKenzie, Kenneth Input Output, United Kingdom Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
David MacQueenMacQueen, David University of Chicago (Emeritus) MsML: A Proposal for a successor ML
Stefan MadaMada, Stefan University of Utah Translation Validation for LLVM's AArch64 Backend
Eduardo MadeiraMadeira, Eduardo LASIGE, University of LisbonPortugal Video Chair in AV Committee for ICFP/SPLASH 2025
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom A guided tour through Oxidized OCaml The Wild West of post-POSIX IO Interfaces Functional Networking for Millions of Docker Desktops (Experience Report) Three steps for OCaml to crest the AI humps Committee Member in Program Committee within the ICFP Student Research Competition-track Generating a corpus of Hazel programs from ill-typed OCaml programs (Extended Abstract) Session Chair of Lightning talks and demos (part of PROPL) A FAIR Case for a Live Computational Commons Scaling the Urban Forest: An Integrated Framework for Managing Cities by Fusing Raster and Vector Data Spatial Programming for Environmental Monitoring Closing thoughts from the chairs Welcome to the 2nd PROPL Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings Programming Opportunities for the Global Biodiversity Observation Network Yirgacheffe: a declarative approach to geospatial data Organizing Committee in Organising Committee within the PROPL-track Decomposable Type Highlighting for Bidirectional Type and Cast Systems
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 Committee Member in Program Committee within the SPLASH Onward! Papers-track
Ole Lehrmann MadsenMadsen, Ole Lehrmann Aarhus UniversityDenmark Committee Member in Program Committee within the SPLASH Onward! Papers-track
José Pedro MagalhãesMagalhães, José Pedro Standard Chartered BankUnited Kingdom Session Chair of Compiler (part of Haskell)
Enrico MagnagoMagnago, Enrico Amazon Web Services Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Shrikha MahantyMahanty, Shrikha Indian Institute of Technology Mandi ScalaF: Functional Refactoring Suggestions for Scala
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
Caleb MalchikMalchik, Caleb Yale University On Collective Control over User Interfaces in the Face of Network Eﬀects
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Efficient Algorithms for the Uniform Tokenization Problem
Tarun ManglaMangla, Tarun Indian Institute Of Technology Delhi STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management
Wensen MaoMao, Wensen Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Mariana MarasoiuMarasoiu, Mariana Gradient Control LaboratoriesUnited Kingdom Committee Member in Program Committee within the PAINT-track
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
Dhruv MarooMaroo, Dhruv IIT Madras, Chennai A Mechanically Verified Garbage Collector for OCaml
Stefan MarrMarr, Stefan Johannes Kepler University LinzAustria Evaluating Candidate Instructions for Reliable Program Slowdown at the Compiler Level - Towards Supporting Fine-grained Slowdown for Advanced Developer Tooling Steering Committee Chair in Organizing Committee within the VMIL-track 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 Python, Is It Being Killed by Incremental Improvements?
Matteo MarraMarra, Matteo Nokia Bell Labs, BelgiumBelgium BabelBridge: A Control-Flow Graph Debugger for Microcontrollers A Control-Flow Graph Approach to Language-Agnostic Debugging for Microcontrollers
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
Danielle MarshallMarshall, Danielle University of GlasgowUnited Kingdom Committee Member in Program Committee within the HOPE-track
Chris MartensMartens, Chris Northeastern UniversityUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track 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
Isabella MastroeniMastroeni, Isabella University of VeronaItaly Relating Distances and Abstractions: An Abstract Interpretation Perspective
Hidehiko MasuharaMasuhara, Hidehiko Institute of Science TokyoJapan Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track 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 Session Chair of Concurrency (part of SPLASH Onward! Papers) Committee Member in Program Committee within the SPLASH Onward! Papers-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track An Interactive Learning Environment for Program Design Daisy: An Exercise Environment for Learning Information Modeling Implementing and Evaluating a High-Level Language with WasmGC and the Wasm Component Model: Scala’s Case Committee Member in Program Committee within the TyDe-track Committee Member in Program Committee within the FUNARCH-track Joy of Meta-Tracing Just-in-Time Compilation: More Than Just a VM Generator
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
Kazutaka MatsudaMatsuda, Kazutaka Tohoku UniversityJapan Committee Member in Program Committee within the miniKanren-track
Toni MattisMattis, Toni University of Potsdam; Hasso Plattner InstituteGermany Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions
Damiano MazzaMazza, Damiano CNRS, LIPN, Université Sorbonne Paris NordFrance Committee Member in ICFP Programme Committee within the ICFP Papers-track
Riccardo MazzaMazza, Riccardo APM SaluzzoItaly Sonic Earth - An Algorithmic Performance Approach to Real-Time Environmental Sonification Concert: Sonic Earth
Conor McBrideMcBride, Conor University of Strathclyde Fulls Seldom Differ
James McCannMcCann, James Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the SPLASH FARM-track 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
Andrew McNuttMcNutt, Andrew University of UtahUnited States Authoring Tools for Transparent Climate Reporting
Sergey MechtaevMechtaev, Sergey Peking UniversityChina Committee Member in Organizing Committee within the LMPL-track
S Hessam M MehrMehr, S Hessam M University of Glasgow TideScript: A Domain Specific Language for Peptide Chemistry
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 End-to-End Compiler Infrastructure for Emerging Tensor Accelerators 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
Eagon MengMeng, Eagon MIT What You See Is What It Does: A Structural Pattern for Legible Software
Ruijie MengMeng, Ruijie National University of Singapore, SingaporeSingapore Large Language Model powered Symbolic Execution
Lucy MenonMenon, Lucy Microsoft Hyperlight-Wasm: Bringing virtualisation-based security to Wasm, and using Wasm at Microsoft
Mira MeziniMezini, Mira TU Darmstadt; hessian.AI; National Research Center for Applied Cybersecurity ATHENEGermany Steering Committee Member in Steering Committee for SPLASH 2025
Jan MidtgaardMidtgaard, Jan IndependentDenmark Property-Based Testing of OCaml 5’s Runtime System: Fun and Segfaults with Interpreters and State Transition Functions Programme Committee in Program Committee within the OlivierFest-track
Benjamin MikekMikek, Benjamin Georgia Institute of Technology Towards Compiler-Guided Static Analysis
Mae MilanoMilano, Mae Princeton UniversityUnited States General Chair in Organizing Committee within the FARM-track Interactive Theorem Provers for Proof Education Session Chair of Performance Evening (part of SPLASH FARM) Session Chair of Math and Music (part of SPLASH FARM) Session Chair of Functional Programming (part of SPLASH FARM) Session Chair of Language Design (part of SPLASH FARM) General Chair in Organizing Committee within the SPLASH FARM-track Session Chair of LGBTQ Lunch (part of ICFP Diversity, Equity, and Inclusion) Bringing Fearless Concurrency to Swift
Stefan MiliusMilius, Stefan Friedrich-Alexander University Erlangen-NürnbergGermany Bialgebraic Reasoning on Stateful Languages
Josh MillarMillar, Josh Imperial College London Spatial Programming for Environmental Monitoring
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
Yaron MinskyMinsky, Yaron The Saga of Multicore OCaml
Mikhail MintsMints, Mikhail California Institute of TechnologyUnited States Compositional Quantum Control Flow with Efficient Compilation in Qunity
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance Committee Member in Program Committee within the SAS -track
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Workshops Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Workshop Co-Chair in Organizing Committee for SPLASH 2025 Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty
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 Committee Member in Program Committee within the SAS -track
Md Rakib Hossain MisuMisu, Md Rakib Hossain University of California IrvineUnited States AutoVerus: Automated Proof Generation for Rust Code
Jacqueline MitchellMitchell, Jacqueline University of Southern California Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Verification Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Jaiaid MobinMobin, Jaiaid Rochester Institute of Technology Memory Tiering in Python Virtual Machine
Sidi Mohamed BeillahiMohamed Beillahi, Sidi University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines Committee Member in Program Committee within the SAS -track
Abdalrhman MohamedMohamed, Abdalrhman Stanford University Interactive Bit Vector Reasoning using Verified Bitblasting
Isidore MohrMohr, Isidore Concert: Girard’s Paradox Girard's Paradox as Structure Music
Alexandre MoineMoine, Alexandre New York UniversityUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Committee Member in Program Committee within the HOPE-track
Evgenii MoiseenkoMoiseenko, Evgenii JetBrains Research Testing concurrent code on JVM with Lincheck
Abtin MolaviMolavi, Abtin University of Wisconsin-Madison Compiling Quantum Circuits Dependency-Aware Compilation for Surface Code Quantum Architectures Graduate Student Panel
Raphaël MonatMonat, Raphaël Inria and University of LilleFrance Committee Member in Program Committee within the SAS -track
Stefan MonnierMonnier, Stefan Université de MontréalCanada Committee Member in Program Committee within the TyDe-track
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 Committee Member in Program Committee within the HATRA-track
José MoralesMorales, José IMDEA Software InstituteSpain Committee Member in Steering Committee within the SAS -track
Marco MorazanMorazan, Marco pc Automatic Invariant Testing for Finite-State Machines
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
Sosuke MoriguchiMoriguchi, Sosuke Institute of Science TokyoJapan Session Chair of Session 3 (part of TyDe) Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search Co-operative JIT Compilation for Resource-Constrained Low-Power Coprocessors
J. Garrett MorrisMorris, J. Garrett University of IowaUnited States Chair's report Welcome Co-chair in Program Committee within the Haskell-track Committee Member in Program Committee within the FUNARCH-track
Nicholas MorrisMorris, Nicholas University of Glasgow TideScript: A Domain Specific Language for Peptide Chemistry
Peter D. MossesMosses, Peter D. Delft University of Technology; Swansea UniversityNetherlands Checking a Denotational Semantics of Scheme in Agda A Compositional Semantics for eval in Scheme Programme Committee in Program Committee within the OlivierFest-track
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Teaching Software Specification (Experience Report) Graduate Student Panel
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 A Verified Thread-Safe Array 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
Niek MullenersMulleners, Niek Utrecht UniversityNetherlands Committee Member in Program Committee within the HATRA-track
Aäron MunstersMunsters, Aäron Vrije Universiteit Brussel Dynamic Analysis Extending a Shadow Runtime for Profit JASMaint: Portable Multi-language Taint Analysis for the Web
Adithya MuraliMurali, Adithya University of Illinois at Urbana-ChampaignUnited States FO-Complete Program Verification for Heap Logics
Yuito MuraseMurase, Yuito Kyoto University, JapanJapan Hygienic Macros via Staged Environment Machines (Position Paper)
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 SPLASH 2025 SIGPLAN Chair in Steering Committee for ICFP 2025
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk)
Hanspeter MössenböckMössenböck, Hanspeter JKU LinzAustria Fast and Compact: Reducing Size of AOT-Compiled Java Code Without Sacrificing Performance
Anders MøllerMøller, Anders Aarhus UniversityDenmark SIGPLAN Vice Chair in Steering Committee for SPLASH 2025 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 A Mechanically Verified Garbage Collector for OCaml
Santosh NagarakatteNagarakatte, Santosh Rutgers UniversityUnited States Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
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 Program Committee within the VMIL-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Keisuke NakanoNakano, Keisuke Tohoku UniversityJapan Committee Member in Program Committee within the Scheme-track
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Committee Member in Steering Committee within the SAS -track
Chandrakana NandiNandi, Chandrakana CertoraUnited States Workshops Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Workshops Co-Chair in Organizing Committee for ICFP 2025 Workshops Co-Chair in Workshop Selection Committee within the ICFP/SPLASH Workshops-track Formalizing Linear Motion G-code for Invariant Checking and Differential Testing of Fabrication Tools
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
Srinivas NarayanaNarayana, Srinivas Rutgers University Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
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 Committee Member in Program Committee within the SAS -track
Amirmohammad NazariNazari, Amirmohammad University of Southern CaliforniaUnited States Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Chrystopher L. NehanivNehaniv, Chrystopher L. University of Waterloo Computational Exploration of Finite Semigroupoids
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 Committee Member in Program Committee within the HATRA-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
Long Tien NguyenNguyen, Long Tien Carnegie Mellon University Unfolding Expressions for Gradual Verification
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 LegoFuzz: Interleaving Large Language Models for Compiler Testing
Mihai NicolaNicola, Mihai Stevens Institute of Technology Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Oscar NierstraszNierstrasz, Oscar feenk.comSwitzerland PC Member in Program Committee within the SPLASH Onward! Essays-track
Dimitrios NikolopoulosNikolopoulos, Dimitrios Virginia TechUnited States Memory Tiering in Python Virtual Machine
Keisuke NishimuraNishimura, Keisuke InriaFrance Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core
Yue NiuNiu, Yue National Institute of Informatics Integrating Resource Analyses via Resource Decomposition
James NobleNoble, James Independent. Wellington, NZNew Zealand Session Chair of Onward! Essays 2 (part of SPLASH Onward! Essays) Reasoning about External Calls Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Session Chair of Onward! Essays 2 (part of SPLASH Onward! Papers) Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities Against Borrowing: Own the forest, not the trees! Committee Member in Organizing Committee within the IWACO-track Fast & Easy ASTs for Flexible Embedded Interpreters
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
Camille NoûsNoûs, Camille Laboratoire Cogitamus - Université PubliqueFrance Towards Metaprogramming Defunctionalization in Rocq
Jose Nuno OliveiraNuno Oliveira, Jose University of Minho; INESC TECPortugal How much is in a square? Calculating functional programs with squares
Clemens Nylandsted KlokmoseNylandsted Klokmose, Clemens Aarhus UniversityDenmark Steering Committee Member in Steering Committee for SPLASH 2025 Onward! Papers Co-chair in Organizing Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Co-chair in Program Committee within the SPLASH Onward! Papers-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
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 Session Chair of Types and monads (part of Haskell) Committee Member in Program Committee within the Haskell-track
Humphrey ObieObie, Humphrey Monash UniversityAustralia Committee Member in Program Committee within the PAINT-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 System Capybara: Capture Tracking for Ownership and Borrowing Where Are We With Scala's Capabilities?
Hakjoo OhOh, Hakjoo Korea UniversitySouth Korea 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 Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Compiler (part of SAS ) Co-chair in Program Committee within the SAS -track
Wonseok OhOh, Wonseok Korea UniversitySouth Korea Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Nicolás Ojeda BärOjeda Bär, Nicolás LexiFiFrance Committee Member in Program Committee within the OCaml-track
Yasuo OkabeOkabe, Yasuo Kyoto University Bringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly Programs
Yuki OkamotoOkamoto, Yuki Shibaura Institute of Technology Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina 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 Normalization by Evaluation for Non-cumulativity Freezing Bidirectional Typing (Extended Abstract)
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 Committee Member in Program Committee within the ML Family Workshop-track A FAIR Case for a Live Computational Commons Session Chair of Session 2 (part of HATRA) Committee Member in Program Committee within the HATRA-track
Steve OneyOney, Steve University of Michigan Committee Member in Program Committee within the SPLASH Onward! Papers-track
Emily OngOng, Emily National University of SingaporeSingapore Siloso: Finding Logic Bugs in RDBMS via Dialect-Adaptable Reference Engine Construction
Dominic OrchardOrchard, Dominic University of Cambridge; University of KentUnited Kingdom Session Chair of Types and Specifications (part of ICFP Papers) Session Chair of Programming for biodiversity and climate (part of PROPL) Towards Modelling and Verification of Coupler Behaviour in Climate Models Closing thoughts from the chairs Welcome to the 2nd PROPL Organizing Committee in Organising Committee within the PROPL-track
Peter-Michael OseraOsera, Peter-Michael Grinnell CollegeUnited States Committee Member in Program Committee within the HATRA-track
Klaus OstermannOstermann, Klaus University of TübingenGermany Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation Committee Member in ICFP Programme Committee within the ICFP Papers-track
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 A Verified Thread-Safe Array in Rust
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Session Chair of Analyze This (part of OlivierFest) Opening More than a Colleague: Celebrating Olivier’s Impact Organizer in Program Committee within the OlivierFest-track Session Chair of Quantum (part of SPLASH OOPSLA) Soundness of Predictive Concurrency Analyses Career Panel
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
Awanish PandeyPandey, Awanish IIT RoorkeeIndia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Orion PapadakisPapadakis, Orion University of ManchesterUnited Kingdom Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Michail PapadimitriouPapadimitriou, Michail University of ManchesterUnited Kingdom Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Zoe ParaskevopoulouParaskevopoulou, Zoe National Technical University of AthensGreece Committee Member in Program Committee within the ML Family Workshop-track
Akash PardeshiPardeshi, Akash University of Illinois at Urbana-ChampaignUnited States End-to-End Compiler Infrastructure for Emerging Tensor Accelerators
Alberto PardoPardo, Alberto Universidad de la Republica, Uruguay Representing Data Structures with Invariants in Haskell: the cases of BST and AVL [Remote]
Sudha ParimalaParimala, Sudha TaridesIndia How the OCaml Community Established Its Code of Conduct Committee Member in Program Committee within the OCaml-track
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 Committee Member in Program Committee within the SAS -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
Tae Hong ParkPark, Tae Hong Purdue UniversityUnited States Program Chair in Organizing Committee within the FARM-track Computers & Music AND Computer Music— An Unlikely [Ongoing] Journey Program Chair in Organizing Committee within the SPLASH FARM-track
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 Deforestation through refunctionalization 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 Committee Member in Competition Judges within the SPLASH Student Research Competition-track Session Chair of Future of OCaml (part of OCaml) Artifact Evaluation Co-Chair in Artifact Evaluation Committe within the ICFP Artifacts-track
Pouya PartowPartow, Pouya Birmingham University Big Steps in Higher-Order Mathematical Operational Semantics
Lorenzo PasiniPasini, Lorenzo University of Torino, ItalyItaly A typed approach to ontology manipulation (experience report)
Radha PatelPatel, Radha MIT CSAIL Finch: Sparse and Structured Tensor Programming with Control Flow
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited States SPLASH-E Co-Chair in Organizing Committee for SPLASH 2025 SPLASH-E Co-Chair in Program Commitee within the SPLASH -E-track Teaching Software Specification (Experience Report) Committee Member in Program Committee within the ICFP Student Research Competition-track
Abhijit PaulPaul, Abhijit Samsung R&D Institute, BangladeshBangladesh Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints (Extended Abstract) [Remote]
Angel Pavlov AngelovPavlov Angelov, Angel Sofia UniversityBulgaria Video Chair in AV Committee for ICFP/SPLASH 2025
Hannes PayerPayer, Hannes Google Committee Member in Program Committee within the MPLR-track
William PaynePayne, William UNC School of Information and Library Science Weft—Enabling Tidal on the Web
Görkem PaçacıPaçacı, Görkem Tacton SystemsSweden Committee Member in Program Committee within the miniKanren-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
Kexin PeiPei, Kexin The University of ChicagoUnited States Committee Member in Program Committee within the LMPL-track
Yu PeiPei, Yu Hong Kong Polytechnic UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Hila PelegPeleg, Hila TechnionIsrael ScooPy: Enhancing Program Synthesis with Nested Example Specifications Committee Member in Program Committee within the HATRA-track
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 Committee within the SPLASH OOPSLA Artifacts-track Committee Member in Program Committee within the OCaml-track Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Daniel PerelmanPerelman, Daniel MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Roly PereraPerera, Roly University of Cambridge/University of BristolUnited Kingdom Committee Member in Program Committee within the PAINT-track Committee Member in Program Committee within the SPLASH Onward! Papers-track Authoring Tools for Transparent Climate Reporting Committee Member in Program Committee within the PROPL-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
Tomas PetricekPetricek, Tomas Charles UniversityCzechia Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track Committee Member in Program Committee within the HATRA-track
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 Join points in practice
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Structural Information Flow: A Fresh Look at Types for Non-Interference
Brysen PfingstenPfingsten, Brysen Seton Hall University Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics
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
Chris PhiferPhifer, Chris GaloisUnited States The CoCompiler: DSL Lifting via Relational Compilation
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 Contextual Equality Saturation Committee Member in Steering Committee within the SAS -track
Christoph PichlerPichler, Christoph Johannes Kepler University LinzAustria Fast and Compact: Reducing Size of AOT-Compiled Java Code Without Sacrificing Performance
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark Synchronous Programming for Kids: A Manifesto What is Fairy Dust? Universal Contracts for WebAssembly
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 Committee Member in Program Committee within the PROPL-track
Frank PiessensPiessens, Frank KU LeuvenBelgium Software Stacks for Confidential Computing Hardware
Maciej PirógPiróg, Maciej University of WrocławPoland Committee Member in Program Committee within the Haskell-track
Alfonso PiscitelliPiscitelli, Alfonso University of Salerno Authoring Tools for Transparent Climate Reporting
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Counterexample-Guided Inference of Modular Specifications Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
Goran PiskachevPiskachev, Goran Amazon Web ServicesGermany Committee Member in Program Committee within the SAS -track
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Committee Member in Program Committee within the HATRA-track
Ian PiumartaPiumarta, Ian Kyoto University of Advanced ScienceJapan Committee Member in Program Committee within the PAINT-track
Matthew PlantPlant, Matthew OneChronos Gouki Scheme: An Embedded Scheme Implementation for Async Rust
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)
Martin PlümickePlümicke, Martin DHBW Stuttgart, Campus Horb, Germany Heterogeneous translation of Scala-like function types in Java-TX
Gabriel PoesiaPoesia, Gabriel Stanford University Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Piotr PolesiukPolesiuk, Piotr University of WrocławPoland Untyped Logical Relations at Work: Control Operators, Contextual Equivalence and Full Abstraction
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Peepco: Batch-Based Consistency Optimization Laurel: Unblocking Automated Verification with Large Language Models
Guillermo PolitoPolito, Guillermo Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStALFrance Committee Member in Program Committee within the SPLASH Onward! Papers-track
Josh PollockPollock, Josh MIT CSAILUnited States Committee Member in Program Committee within the HATRA-track
Andrey PoppPopp, Andrey Ahrefs Committee Member in Program Committee within the OCaml-track
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 Comfy Chair in Organizing Committee for ICFP/SPLASH 2025 Steering Committee Chair in Steering Committee for SPLASH 2025 [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award 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 X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering A Verified Thread-Safe Array in Rust
François PottierPottier, François InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Ari PrakashPrakash, Ari Northeastern UniversityUnited States miniDusa: An Extensible Finite-Choice Logic Programming Language (Lightning Talk)
Jyoti PrakashPrakash, Jyoti University of PassauGermany Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Pontakorn PrasertsukPrasertsuk, Pontakorn Singapore Evolving How We Teach Memory Models
Polyvios PratikakisPratikakis, Polyvios University of CreteGreece MaTSa: Race Detection in Java SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Eli PregersonPregerson, Eli Stony Brook University [CANCELED] Adaptive Search Synthesis as a Recursion Scheme
Daphne Preston-KendalPreston-Kendal, Daphne Scheme Reports at Fifty: Where do we go from here?
Thomas S. PricePrice, Thomas S. Carnegie Mellon UniversityUnited States Polynomial-Time Program Equivalence for Machine Knitting
Maurizio ProiettiProietti, Maurizio IASI-CNRItaly Redundancy Checking in Reversible Flowcharts via Logic-Based Operational Semantics Programme Committee in Program Committee within the OlivierFest-track
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
Angel Luis Scull PupoPupo, Angel Luis Scull Vrije Universiteit Brussel Dynamic Analysis Extending a Shadow Runtime for Profit JASMaint: Portable Multi-language Taint Analysis for the Web
Q Yong Qi FooQi Foo, Yong National University of SingaporeSingapore Pushing the Information-Theoretic Limits of Random Access Lists
Shengchao QinQin, Shengchao Xidian UniversityChina Preguss: It Analyzes, It Specifies, It Verifies
Xueying QinQin, Xueying University of Southern DenmarkDenmark Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Committee Member in Program Committee within the SAS -track
Weihao QuQu, Weihao University at Buffalo, SUNY Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Paola QuagliaQuaglia, Paola University of TrentoItaly More than a Colleague: Celebrating Olivier’s Impact
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 Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Dimi RacordonRacordon, Dimi EPFL, LAMPSwitzerland PC Member in Program Committee within the SPLASH Onward! Essays-track
Dimi RacordonRacordon, Dimi EPFLSwitzerland Existentialize your Generics
Dimi RacordonRacordon, Dimi EPFL, LAMPSwitzerland Round table on ownership challenges Committee Member in Organizing Committee within the IWACO-track Existentialize your Generics Committee Member in Program Committee within the MPLR-track Taking away Mutation The Quest for Mutable Value Semantics in Scala Capability-Safe Erasure in Scala Committee Member in Program Committee within the The Scala Workshop-track
Gabriel RadanneRadanne, Gabriel InriaFrance Committee Member in Program Committee within the OCaml-track
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
M. Mustafa RafiqueRafique, M. Mustafa Rochester Institute of Technology Memory Tiering in Python Virtual Machine
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited States Gauguin, Descartes, Bayes: A Diurnal Golem's Brain 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
Samar RahmouniRahmouni, Samar Inria & Ecole PolytechniqueFrance Video Chair in AV Committee for ICFP/SPLASH 2025
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
Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Boston UniversityUnited States Video Chair in AV Committee for ICFP/SPLASH 2025 Sound Default-Typed Scheme (Position Paper)
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Committee Member in Program Committee within the TyDe-track
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 PC Member in Program Committee within the SPLASH Onward! Essays-track Translation Validation for LLVM's AArch64 Backend
Björn RegnellRegnell, Björn Lund UniversitySweden Committee Member in Program Committee within the The Scala Workshop-track
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
Fermin ReigReig, Fermin Session Chair of Compiler & Runtime (part of OCaml)
Hamza RemmalRemmal, Hamza EPFL, LAMPSwitzerland Existentialize your Generics Session Chair of Capabilities and ownership in Scala (part of IWACO) Existentialize your Generics Session Chair of Noon (part of The Scala Workshop) Session Chair of Afternoon (part of The Scala Workshop) Session Chair of Morning (part of The Scala Workshop) Welcome to Scala'25 Capability-Safe Erasure in Scala Organizer in Organizing Committee within the The Scala Workshop-track
Lisa RennelsRennels, Lisa University of California at BerkeleyUnited States Committee Member in Program Committee within the PROPL-track
Alexander RepenningRepenning, Alexander University of Colorado, BoulderUnited States Committee Member in Program Committee within the SPLASH Onward! Papers-track
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 Range-Analysis-Based Optimization for SML/NJ
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
Francesca A. RidleyRidley, Francesca A. Newcastle University Yirgacheffe: a declarative approach to geospatial data
Manuel RiggerRigger, Manuel National University of SingaporeSingapore Outdoor Activities Chair in Organizing Committee for ICFP/SPLASH 2025 Flexible and Expressive Typed Path Patterns for GQL Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track SQLancer: From Research Prototype to Industry Use
Kenji RikitakeRikitake, Kenji Kenji Rikitake Professional Engineer's Office Committee Member in Program Committee within the Erlang-track
Talia Lily RingerRinger, Talia Lily University of Illinois Urbana-ChampaignUnited States Proof Repair across Quotient Type Equivalences
Xavier RivalRival, Xavier Inria - CNRS - Ecole Normale Superieure de Paris - PSL UniversityFrance Session Chair of Proof we need. Proof! (part of OlivierFest) On the Structure of Abstract Interpreters Programme Committee in Program Committee within the OlivierFest-track Session Chair of Abstraction and Proofs (part of SAS ) Towards static analyses and abstract domains for hyperproperties Committee Member in Program Committee within the SAS -track
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
Alice RixteRixte, Alice Generalizing Turtle Geometry: An Extensible Language for Vector Graphics Drawing
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Program Chair in Program Committee within the FUNARCH-track
Robby Robby Kansas State UniversityUnited States Danvy’s Mystery Functions in Slang
Nicolas RodriguezRodriguez, Nicolas Instituto de Computación, Universidad de la República Representing Data Structures with Invariants in Haskell: the cases of BST and AVL [Remote]
Carlos Rojas CastilloRojas Castillo, Carlos Vrije Universiteit Brussel BabelBridge: A Control-Flow Graph Debugger for Microcontrollers A Control-Flow Graph Approach to Language-Agnostic Debugging for Microcontrollers
Neil RolnickRolnick, Neil Concert: Mirages
Tiark RompfRompf, Tiark Purdue UniversityUnited States Data-Centric Functional Programming with First-Class Finite Maps and Tabulated Abstractions Modeling Reachability Types with Logical Relations -- Semantic Type Soundness, Termination, Effect Safety, and Equational Theory Complete the Cycle: Reachability Types with Expressive Cyclic References Committee Member in ICFP Programme Committee within the ICFP Papers-track
Julian RosemannRosemann, Julian Saarland University, Saarland Informatics CampusGermany Non-interference Preserving Optimising Compilation
Andreas RossbergRossberg, Andreas IndependentGermany [Keynote] Keynote and SpecTec demo
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 Committee Member in Program Committee within the SPLASH Onward! Papers-track
Jurriaan RotRot, Jurriaan Radboud University Nijmegen A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Emanuele RovarettoRovaretto, Emanuele University of Torino, Italy A typed approach to ontology manipulation (experience report)
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 DDMon: a Monitoring Tool for Distributed Deadlock Detection
Craig RoyRoy, Craig Quantinuum Fulls Seldom Differ
Subhajit RoyRoy, Subhajit IIT KanpurIndia Student Research Competition Chair in Organizing Committee for SPLASH 2025 Memory-Safety Verification of Open Programs With Angelic Assumptions SPLASH SRC Awards Co-chair in Review Committee within the SPLASH Student Research Competition-track
Julia RubinRubin, Julia The University of British ColumbiaCanada Committee Member in Program Committee within the LMPL-track
Fabian RuchRuch, Fabian UnaffiliatedSweden Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Gergely RudaRuda, Gergely evosoft Hungary Kft. Evaluating AtomVM for Fault-Tolerant ESP32-Based Systems
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 Committee within the SPLASH OOPSLA Artifacts-track Committee Member in Artifact Evaluation Committe within the ICFP 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/SPLASH 2025 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 Steering Committee Member in Steering Committee for SPLASH 2025 OOPSLA Review Committee Co-Chair in Organizing Committee for SPLASH 2025 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 Committee Member in Program Committee within the WebAssembly Workshop-track P4-SpecTec: A Language Mechanization Framework for P4
Didier RémyRémy, Didier Inria Implicit modules, a middle step towards modular implicits
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 A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free Committee Member in Program Committee within the ICFP Student Research Competition-track
Ken SakayoriSakayori, Ken University of TokyoJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
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
Adrian SampsonSampson, Adrian Cornell University PC Member in Program Committee within the SPLASH Onward! Essays-track
Ashley SamuelsonSamuelson, Ashley University of Wisconsin-MadisonUnited States Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Mateo SanabriaSanabria, Mateo Universidad de los Andes Moving Objects and Behavior Safely in Ad hoc Networks
Takahiro SanadaSanada, Takahiro Fukui Prefectural UniversityJapan Committee Member in Program Committee within the HOPE-track
David SananSanan, David Singapore Institute of TechnologySingapore A complete formal semantics of eBPF instruction set architecture for Solana
Rafaello SannaSanna, Rafaello Harvard UniversityUnited States Beyond Cons: Purely Relational Data Structures
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
Igor Moreno SantosSantos, Igor Moreno USI LuganoSwitzerland TIDE: An Educational Live Programming Environment to Compose Graphics with PyTamaro
Yasmin Chandini SaritaSarita, Yasmin Chandini UIUC Automated Verification of Soundness of DNN Certifiers
Koich SasadaSasada, Koich Stores, Inc.Japan ASTro: An AST-based Reusable Optimization Framework Committee Member in Program Committee within the MPLR-track
Isao SasanoSasano, Isao Shibaura Institute of TechnologyJapan Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust
Kartik SathyanarayananSathyanarayanan, Kartik Netflix, Inc. Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Ryosuke SatoSato, Ryosuke Tokyo University of Agriculture and TechnologyJapan Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
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 X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction Engineering
Roland SchatzSchatz, Roland Oracle Labs Fast and Compact: Reducing Size of AOT-Compiled Java Code Without Sacrificing Performance
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 Constrained generation of well-typed programs (Extended Abstract) [Remote]
Markus SchlegelSchlegel, Markus Active Group GmbHGermany Evolution of Functional UI Paradigms
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
David SchmidtSchmidt, David Kansas State UniversityUnited States More than a Colleague: Celebrating Olivier’s Impact
Julian SchmidtSchmidt, Julian Baden-Wuerttemberg Cooperative State University Heterogeneous translation of Scala-like function types in Java-TX
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
Dominik SchrempfSchrempf, Dominik Well-Typed LLPAustria Automatic C bindings generation for Haskell
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Effectful Lenses: There and Back with Different Monads Staging Automatic Differentiation with Fusion Compositions for Free: Reasoning about Effectful Lenses
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 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 Multiple Resumptions and Local Mutable State, Directly
David J. ScottScott, David J. Docker, Inc. Functional Networking for Millions of Docker Desktops (Experience Report)
Ryan ScottScott, Ryan Galois, Inc.United States Committee Member in Program Committee within the FUNARCH-track
Remy SeassauSeassau, Remy InriaFrance Formal Semantics and Program Logics for a Fragment of OCaml
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Verifying Effectful Programs via Answer-Type Modification On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning Co-chair in Program Committee within the HOPE-track
Koushik SenSen, Koushik University of California at BerkeleyUnited States Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad
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 ICFP General Chair and Local Chair in Organizing Committee for ICFP/SPLASH 2025 ICFP General Chair and Local Chair in Organizing Committee for SPLASH 2025 General Chair in Organizing Committee for ICFP 2025 ICFP'25 General Chair in Steering Committee for ICFP 2025 Opening Organizer in Program Committee within the OlivierFest-track Inductive Synthesis of Inductive Heap Predicates General Chair Report Opening Award Ceremony Session Chair of Monday ICFP Keynote (part of ICFP Keynotes) Multi-Modal Verification of Distributed Systems in Lean
Manuel SerranoSerrano, Manuel Inria; Université Côte d’AzurFrance Chair in Distinguished Papers Committee for ICFP 2025 Session Chair of Memory (part of SPLASH OOPSLA) Float Self-Tagging Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Associate Chair in ICFP Programme Committee within the ICFP Papers-track A Snapshot of the Performance of Wasm Backends for Managed Languages
Sanjit A. SeshiaSeshia, Sanjit A. University of California, BerkeleyUnited States Checking Observational Correctness of Database Systems
Aaditeshwar SethSeth, Aaditeshwar Indian Institute Of Technology Delhi STACD: STAC Extension with DAGs for Geospatial Data and Algorithm Management GPU-accelerated Hydrology Algorithms for On-prem Computation: Flow accumulation, Drainage lines, Watershed delineation, Runoff simulation Committee Member in Program Committee within the PROPL-track
Yasser ShaabanShaaban, Yasser WorkatoUnited States Vibe Coding Needs Vibe Reasoning – Improving Vibe Coding with Formal Verification
Matan ShachnaiShachnai, Matan Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Bhakti ShahShah, Bhakti University of St. Andrews Imperative Syntax for Dependent Types
Prerakkumar Mukeshkumar ShahShah, Prerakkumar Mukeshkumar Catalyst Management Services Pvt. Ltd. Precision Action Towards Climate and Health (PATCH)
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Compressed and Parallelized Structured Tensor Algebra ScaIR: Type-safe Compiler Framework Compatible with MLIR Committee Member in Program Committee within the The Scala Workshop-track
Sheera ShamsuShamsu, Sheera IIT MadrasIndia Session Chair of Community & Ecosystem (part of OCaml) A Mechanically Verified Garbage Collector for OCaml Committee Member in Program Committee within the OCaml-track
Chung-chieh ShanShan, Chung-chieh Indiana UniversityUnited States Committing to the bit: Relational programming with semiring arrays and SAT solving
Arindam SharmaSharma, Arindam Imperial College London P³: Reasoning about Patches via Product Programs
Dongdong SheShe, Dongdong HKUST (The Hong Kong University of Science and Technology)Hong Kong SAR China Publications Chair in Organizing Committee for SPLASH 2025
Gan ShenShen, Gan University of California at Santa CruzUnited States Freer Arrows and Why You Need Them in Haskell
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 Automated Approaches for Software Migration and Evolution
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
Stephen SherrattSherratt, Stephen Tarides Software-defined declarative synthesizer live-coding in a jupyter notebook OCaml Package Management with (only!) Dune
Darshal ShettyShetty, Darshal Indiana University Gradual Metaprogramming
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
Ling ShiShi, Ling Nanyang Technological UniversitySingapore Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
Qingkai ShiShi, Qingkai Nanjing UniversityChina An Empirical Study of Bugs in the rustc Compiler Committee Member in Organizing Committee within the LMPL-track Session Chair of Software Engineering (part of Sponsor Invited Talks) Organizer in Organizing Committee within the Sponsor Invited Talks-track
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 Scheme-track Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages Committee Member in Program Committee within the ICFP Student Research Competition-track
Kazuyuki ShudoShudo, Kazuyuki Kyoto UniversityJapan Bringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly Programs
Xujie SiSi, Xujie University of Toronto Committee Member in Program Committee within the SAS -track Toward Repository-Level Program Verification with Large Language Models A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Filip SieczkowskiSieczkowski, Filip Heriot-Watt UniversityUnited Kingdom Committee Member in Program Committee within the ML Family Workshop-track
Jeremy G. SiekSiek, Jeremy G. Indiana UniversityUnited States Committee Member in Distinguished Papers Committee for ICFP 2025 Verified Nanopasses for Compiling Conditionals Programme Committee in Program Committee within the OlivierFest-track Session Chair of Gradual Typing and Security (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Session 1 (part of TyDe) Gradual Metaprogramming
Cedric SiemsSiems, Cedric Ruhr University Bochum Detecting and explaining (in-)equivalence of context-free grammars
Ho Siew FoongSiew Foong, Ho National University of SingaporeSingapore Local Arrangements Chair in Organizing Committee for ICFP/SPLASH 2025 Local Arrangements Chair in Organizing Committee for SPLASH 2025
Jesse SigalSigal, Jesse University of EdinburghUnited Kingdom Author in Artifact Evaluation Committe within the ICFP Artifacts-track
Mihaela SighireanuSighireanu, Mihaela University Paris-Saclay, ENS Paris-Saclay, CNRS, LMFFrance Steering Committee Member in Steering Committee for SPLASH 2025 Committee Member in Steering Committee within the SAS -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
Jeremy SingerSinger, Jeremy University of GlasgowUnited Kingdom Let's Take Esoteric Programming Languages Seriously Session Chair of Research Paper 3 & Tools (part of MPLR) Committee Member in Program Committee within the MPLR-track
Abhishek Kr SinghSingh, Abhishek Kr IIIT HyderabadSingapore 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 Committee Member in Program Committee within the SAS -track Committee Member in Steering Committee within the SAS -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/SPLASH 2025 Diversity Co-Chair in Organizing Committee for ICFP 2025 Diversity Co-Chair in Steering Committee for ICFP 2025 A guided tour through Oxidized OCaml 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 Session Chair of Implementation (part of ICFP Papers) Committee Member in ICFP Programme Committee within the ICFP Papers-track A Mechanically Verified Garbage Collector for OCaml Session Chair of Principled scientific programming (part of PROPL) Closing thoughts from the chairs Welcome to the 2nd PROPL PC Chair in Program Committee within the PROPL-track Committee Member in Program Committee within the FUNARCH-track
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)
Calvin SmithSmith, Calvin University of Texas AustinUnited States Committee Member in Review Committee within the SPLASH Student Research Competition-track
Sunbeom SoSo, Sunbeom GIST (Gwangju Institute of Science and Technology) Committee Member in Program Committee within the SAS -track
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 Committee Member in Program Committee within the SAS -track
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 From Delimited Continuations to Staged Logics SRC Judge & Co-Organizer in Review Committee within the SPLASH Student Research Competition-track SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Testing and Constraint Solving (part of SAS ) Specifying and Verifying Future Conditions Committee Member in Program Committee within the OCaml-track Committee Member in Program Committee within the HOPE-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 Literate Tracing
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
Naomi SpargoSpargo, Naomi Galois, Inc. Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces The CoCompiler: DSL Lifting via Relational Compilation
Oscar SpencerSpencer, Oscar [Keynote] Wasm GC and the Future of High-Level Language Compilation
Michael SperberSperber, Michael Active Group GmbHGermany PC Member in Program Committee within the SPLASH Onward! Essays-track Six Years of FUNAR: Functional Training for Software Architects Evolution of Functional UI Paradigms
Arnaud SpiwackSpiwack, Arnaud TweagFrance Invertible Syntax without the Tuples (Functional Pearl) Programme Committee in Program Committee within the OlivierFest-track Destination calculus: A linear λ-calculus for purely functional memory writes Session Chair of Keynote + Research paper (part of Haskell) Committee Member in Program Committee within the Haskell-track
Manu SridharanSridharan, Manu University of California at RiversideUnited States Steering Committee Member in Steering Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Michael StaabStaab, Michael University of Freiburg Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly
Caleb StanfordStanford, Caleb University of California, DavisUnited States Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Artem StarikovStarikov, Artem Innopolis University typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell
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 Certified Decision Procedures for Width-Independent Bitvector Predicates Interactive Bit Vector Reasoning using Verified Bitblasting Session Chair of Separation Logic (part of ICFP Papers)
Friedrich SteimannSteimann, Friedrich Fernuniversität in HagenGermany PC Member in Program Committee within the SPLASH Onward! Essays-track
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 Programming Language Design for GPU Systems
Isabella StilkerichStilkerich, Isabella Schaeffler TechnologiesGermany Committee Member in Program Committee within the FUNARCH-track
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 Abstracting Concolic Execution for Soft Contract Verification
Athanasios StratikopoulosStratikopoulos, Athanasios University of ManchesterUnited Kingdom Committee Member in Program Committee within the VMIL-track Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Filip StrömbäckStrömbäck, Filip Linköping UniversitySweden Continuations for All: Language Design Considerations for Accessible Continuations
Abel StukerStuker, Abel Vrije Universiteit Brussel JASMaint: Portable Multi-language Taint Analysis for the Web
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
Ting SuSu, Ting East China Normal UniversityChina Committee Member in Program Committee within the LMPL-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 In the Specifications We Pursue
Giancarlo SucciSucci, Giancarlo Committee Member in Program Committee within the SPLASH Onward! Papers-track
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 Student Research Competition Chair in Organizing Committee for SPLASH 2025 Efficient Abstract Interpretation via Selective Widening SPLASH SRC Awards Co-chair in Review Committee within the SPLASH Student Research Competition-track Co-chair in Program Committee within the SAS -track Committee Member in Program Committee within the LMPL-track
Matúš SulírSulír, Matúš Technical University of KošiceSlovakia RuntimeSave: A Graph Database of Runtime Values
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 AI Safety through Programming? Keynote Speaker in Keynote Speaker within the LMPL-track
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
Yi SunSun, Yi Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
Kirshanthan SundararajahSundararajah, Kirshanthan Virginia TechUnited States Memory Tiering in Python Virtual Machine
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 Carnegie Mellon University PLMW Co-Chair in Organizing Committee for ICFP/SPLASH 2025
Milijana SurbatovichSurbatovich, Milijana University of Maryland Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Session Chair of Women in PL Dinner (part of ICFP Diversity, Equity, and Inclusion) PLMW Welcome Committee Member in Program Committee within the PLMW @ ICFP/SPLASH-track
Go SuzukiSuzuki, Go Institute of Science TokyoJapan Co-operative JIT Compilation for Resource-Constrained Low-Power Coprocessors
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 A Layered Certifying Compiler Architecture
Rebecca SwordsSwords, Rebecca Gable.aiUnited States Committee Member in Program Committee within the miniKanren-track
Emma SöderbergSöderberg, Emma Lund UniversitySweden Committee Member in Program Committee within the PAINT-track Committee Member in Program Committee within the SPLASH Onward! Papers-track
T Marco T MorazanT Morazan, Marco Seton Hall UniversityUnited States Committee Member in Program Committee within the Scheme-track Derivation Visualization for Context-Free Grammar Design: Helping Students Understand Context-Free Grammars
Nicolas TabareauTabareau, Nicolas InriaFrance Incremental Certified Programming Robust Dynamic Embedding for Gradual Typing
Marcel TaeumelTaeumel, Marcel University of Potsdam; Hasso Plattner InstituteGermany Steering Committee Member in Steering Committee for SPLASH 2025 Block-based Editing in a Textual World Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Gourav TakharTakhar, Gourav Indian Institute of Technology - KanpurIndia Memory-Safety Verification of Open Programs With Angelic Assumptions SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track
Satoshi TakimotoTakimoto, Satoshi Institute of Science TokyoJapan Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search
Jean-Pierre TalpinTalpin, Jean-Pierre INRIA, France HpC: A Calculus for Hybrid and Mobile Systems
Raiki TamuraTamura, Raiki Kyoto UniversityJapan Bringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly Programs
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 Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad
Tian TanTan, Tian Nanjing UniversityChina Two Approaches to Fast Bytecode Frontend for Static Analysis Committee Member in Program Committee within the SAS -track
Yong Kiam TanTan, Yong Kiam *Institute for Infocomm Research, ASTAR** From CakeML to Proof Checking, and Back Again Committee Member in Program Committee within the ML Family Workshop-track
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 Freezing Bidirectional Typing (Extended Abstract) Rows and Capabilities as Modal Effects (Extended Abstract)
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
Rikito TaniguchiTaniguchi, Rikito VirtusLab and Institute of Science TokyoJapan Implementing and Evaluating a High-Level Language with WasmGC and the Wasm Component Model: Scala’s Case
Steven TanimotoTanimoto, Steven University of Washington, SeattleUnited States Committee Member in Program Committee within the PAINT-track
Swamit TannuTannu, Swamit University of Wisconsin-Madison Compiling Quantum Circuits Dependency-Aware Compilation for Surface Code Quantum Architectures
Éric TanterTanter, Éric University of ChileChile Incremental Certified Programming Robust Dynamic Embedding for Gradual Typing
Muhammad Usman TariqTariq, Muhammad Usman Stanford University REPTILE: Performant Tiling of Recurrences
Simon TarrTarr, Simon IUCN Yirgacheffe: a declarative approach to geospatial data
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
Ramsay TaylorTaylor, Ramsay IOGUnited Kingdom A Tale of Two Zippers
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Mohit TekriwalTekriwal, Mohit Lawrence Livermore National LaboratoryUnited States Committee Member in Program Committee within the SAS -track
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States Gauguin, Descartes, Bayes: A Diurnal Golem's Brain 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 SRC Judge & Co-Organizer in Competition Judges within the SPLASH Student Research Competition-track Committee Member in Program Committee within the SAS -track ScalaF: Functional Refactoring Suggestions for Scala
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/SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for ICFP 2025 Student Volunteer Chair in Organizers within the ICFP/SPLASH Volunteers-track
Suhas ThalankiThalanki, Suhas Carnegie Mellon University Debugging WebAssembly? Put some Whamm on it!
Lauritz ThamsenThamsen, Lauritz University of GlasgowUnited Kingdom Committee Member in Program Committee within the PROPL-track
Christoph ThiedeThiede, Christoph Hasso Plattner Institute, University of Potsdam, GermanyGermany Toward Bridging the Tool Gap: Equipping Large Language Models with Tools to Answer Programmers’ Questions
Peter ThiemannThiemann, Peter University of FreiburgGermany Session Chair of It’s All a Matter of Interpretation! (part of OlivierFest) What I Always Wanted to Know about Second Class Values Programme Committee in Program Committee within the OlivierFest-track Session Chair of Proofs (part of SPLASH OOPSLA) Borrowing From Session Types Associate Chair in ICFP Programme Committee within the ICFP Papers-track Session Chair of Tuesday ICFP Keynote (part of ICFP Keynotes) Committee Member in Organizing Committee within the IWACO-track Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly
Thore ThießenThießen, Thore University of Münster Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements
William ThomasThomas, William Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Simon ThompsonThompson, Simon University of Kent (UK)United Kingdom Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
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 Supercharge Compiler Engineering with LLMs
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
Frank TipTip, Frank Northeastern UniversityUnited States Steering Committee Member in Steering Committee for SPLASH 2025
Tanmay TirpankarTirpankar, Tanmay University of Utah Translation Validation for LLVM's AArch64 Backend
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited States Rebase Co-chair in Organizing Committee for SPLASH 2025 WebAssembly Research Tools Tutorial Unveiling Heisenbugs with Diversified Execution Debugging WebAssembly? Put some Whamm on it! Committee Member in Program Committee within the WebAssembly Workshop-track Session Chair of REBASE (part of REBASE) Session Chair of REBASE (part of REBASE) Session Chair of REBASE (part of REBASE) Committee Member in Organizing Committee within the REBASE-track
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 NOVA-LINCS; Nova University of LisbonPortugal Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Bernardo ToninhoToninho, Bernardo Instituto Superior Técnico - University of LisbonPortugal Fusing Session-Typed Concurrent Programming into Functional Programming
Cassia TorczonTorczon, Cassia University of Pennsylvania QED in Context: An Observation Study of Proof Assistant Users
Hazel TorekTorek, Hazel Clemson UniversityUnited States Unfolding Expressions for Gradual Verification
Matías ToroToro, Matías University of ChileChile Flexible and Expressive Typed Path Patterns for GQL Robust Dynamic Embedding for Gradual Typing Committee Member in ICFP Programme Committee within the ICFP Papers-track
Jay TorryTorry, Jay University of Cambridge Should we use LLMs to program for the planet?
Yota ToyamaToyama, Yota Canada Stak Scheme: The tiny R7RS-small implementation
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)
Sophia TuranoTurano, Sophia Seton Hall University Automatic Invariant Testing for Finite-State Machines
Gergő Lajos TuránTurán, Gergő Lajos Eötvös Loránd University Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Mechanised Proofs of Atom Exhaustion in Erlang
Saar Tzour-ShadayTzour-Shaday, Saar Technion – Israel Institute of TechnologyIsrael Mini-Batch Robustness Verification of Deep Neural Networks
Melinda TóthTóth, Melinda Eötvös Loránd UniversityHungary Securing Erlang and Elixir applications Evaluating AtomVM for Fault-Tolerant ESP32-Based Systems
U Thien UdomsrirungruangUdomsrirungruang, Thien University of Oxford qblaze: An Efficient and Scalable Sparse Quantum Simulator
Tomoharu UgawaUgawa, Tomoharu University of TokyoJapan Committee Member in Program Committee within the VMIL-track Session Chair of Languages (part of SPLASH Onward! Papers) Session Chair of MPLR Keynote & Research Paper 2 (part of MPLR) PC Chair in Program Committee within the MPLR-track
Hiroshi UnnoUnno, Hiroshi Tohoku UniversityJapan On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs Committee Member in ICFP Programme Committee within the ICFP Papers-track
Caterina UrbanUrban, Caterina Inria & ENS \| PSLFrance Relating Distances and Abstractions: An Abstract Interpretation Perspective Committee Member in Program Committee within the SAS -track Committee Member in Steering Committee within the SAS -track Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis
Bernhard Urban-ForsterUrban-Forster, Bernhard Oracle LabsAustria Fast and Compact: Reducing Size of AOT-Compiled Java Code Without Sacrificing Performance
Henning UrbatUrbat, Henning Friedrich-Alexander University Erlangen-NürnbergGermany Session Chair of Semantics (part of ICFP Papers) Bialgebraic Reasoning on Stateful Languages
Ana Denisa UrleaUrlea, Ana Denisa Romanian Air Traffic Services Administration Bridging Disciplinary Gaps in Climate Research Through Programming Accessibility and Interdisciplinary Collaboration
Cristian UrleaUrlea, Cristian University Of Glasgow Bridging Disciplinary Gaps in Climate Research Through Programming Accessibility and Interdisciplinary Collaboration
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
Milla ValnetValnet, Milla Sorbonne UniversitéFrance Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Isaac van Bakelvan Bakel, Isaac ETH ZurichSwitzerland Modular Reasoning about Global Variables and Their Initialization
Xavier Van de WoestyneVan de Woestyne, Xavier TaridesFrance A New Era of OCaml Editing: Powered by Merlin, Delivered via LSP
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
Andre van der Hoekvan der Hoek, Andre University of California, IrvineUnited States PC Member in Program Committee within the SPLASH Onward! Essays-track
Tijs van der Stormvan der Storm, Tijs CWI & University of GroningenNetherlands Committee Member in Program Committee within the PAINT-track Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Committee Member in Program Committee within the SPLASH Onward! Papers-track Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Noah Van EsVan Es, Noah Sofware Languages Lab, Vrije Universiteit BrusselBelgium Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Jacob Van GeffenVan Geffen, Jacob Veridise Inc. Scalable and Accurate Application-level Crash-Consistency Testing via Representative Testing
Riemer van Rozenvan Rozen, Riemer CWINetherlands Committee Member in Program Committee within the PAINT-track
Eric Van WykVan Wyk, Eric University of Minnesota, Twin CitiesUnited States Steering Committee Member in Steering Committee for SPLASH 2025
Bram VandenbogaerdeVandenbogaerde, Bram Software Languages Lab, Vrije Universiteit BrusselBelgium Abstracting Concolic Execution for Soft Contract Verification Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Frederik VandeputteVandeputte, Frederik Nokia Bell Labs Foundational Design Principles and Patterns for Building Robust & Adaptive GenAI-Native Systems
Wim VanderbauwhedeVanderbauwhede, Wim University of Glasgow Bridging Disciplinary Gaps in Climate Research Through Programming Accessibility and Interdisciplinary Collaboration
Grant VanDomelenVanDomelen, Grant Portland State University, USA Freer Arrows and Why You Need Them in Haskell
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 Steering Committee Member in Steering Committee for SPLASH 2025 Steering Committee Member in Onward! Steering Committee within the SPLASH Onward! Essays-track Borrowing From Session Types Session Chair of Tools (part of SPLASH Onward! Papers) Steering Committee Member in Steering Committee within the SPLASH Onward! Papers-track
Martin VechevVechev, Martin ETH ZurichSwitzerland qblaze: An Efficient and Scalable Sparse Quantum Simulator
Jyothi VeduradaVedurada, Jyothi IIT HyderabadIndia Committee Member in Review Committee within the SPLASH Student Research Competition-track
Andreas VenerisVeneris, Andreas University of TorontoCanada HEMVM: a Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Arnaud VenetVenet, Arnaud Meta Gradual Metaprogramming
Hristo VenevVenev, Hristo INSAIT, Sofia University "St. Kliment Ohridski"Bulgaria qblaze: An Efficient and Scalable Sparse Quantum Simulator
Nitish Kumar VenkatesanVenkatesan, Nitish Kumar Catalyst Management Services Pvt. Ltd. Precision Action Towards Climate and Health (PATCH)
Mauricio Verano MerinoVerano Merino, Mauricio Vrije Universiteit AmsterdamNetherlands Organizer in Organizing Committee within the PAINT-track Committee Member in Program Committee within the PAINT-track
Sarah VerbelenVerbelen, Sarah Vrije Universiteit Brussel, Belgium Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell
Ekaterina VerbitskaiaVerbitskaia, Ekaterina JetBrains Research; Constructor University BremenNetherlands Session Chair of Extending miniKanren and Relational Programming (part of miniKanren) Typed Embedding of miniKanren for Functional Conversion
Marcos VieraViera, Marcos University of the Republic, Uruguay Representing Data Structures with Invariants in Haskell: the cases of BST and AVL [Remote]
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
Harishankar VishwanathanVishwanathan, Harishankar Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States Checking $\delta$-Satisfiability of Reals with Integrals
Jan VitekVitek, Jan Northeastern UniversityUnited States Comfy Chair in Organizing Committee for ICFP/SPLASH 2025 Steering Committee Chair in Steering Committee for SPLASH 2025 Copy-and-Patch Just-in-Time Compiler for R
Samuel VivienVivien, Samuel INRIA & PSL Implicit modules, a middle step towards modular implicits
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
Adriana Laura VoineaVoinea, Adriana Laura University of Glasgow, UKUnited Kingdom Bridging Disciplinary Gaps in Climate Research Through Programming Accessibility and Interdisciplinary Collaboration Session Chair of Welcome & Keynote (part of Erlang) Session Chair of Distributed Behaviour (part of Erlang) Mailboxer: Static Detection of Erlang Communication Errors Welcome to Erlang’25 Closing Remarks Organizing Committee in Organizing Committee within the Erlang-track
Dmitri VolkovVolkov, Dmitri Indiana University Committing to the bit: Relational programming with semiring arrays and SAT solving
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 Tale of Two Zippers Programme Committee in Program Committee within the OlivierFest-track [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Committee Member in Program Committee and Panel within the SPLASH Doctoral Symposium-track Session Chair of Parametricity (part of ICFP Papers) A simple blame calculus for explicit nulls Haskell equations, thirty-eight years later Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
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 Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Chaozheng WangWang, Chaozheng The Chinese University of Hong Kong Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps
Chengpeng WangWang, Chengpeng Purdue UniversityUnited States Committee Member in Organizing Committee within the LMPL-track
Claire WangWang, Claire University of Pennsylvania Rocq N'Roll Concert: RocqNRoll
Di WangWang, Di Peking UniversityChina Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials Composable Effect Handling for Programming LLM-integrated Scripts Committee Member in Program Committee within the TyDe-track CStar: Unifying Programming and Verification in C
Edward WangWang, Edward Massachusetts Institute of Technology Lessons from Building a Hardware Compiler in Scala 3: A Practitioner Perspective
Hanzhang WangWang, Hanzhang Fudan University, ChinaChina JavART: a Lightweight Rule-Based JIT Compiler Using Translation Rules Extracted from a Learning Approach
Haoyu WangWang, Haoyu Huazhong University of Science and TechnologyChina Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
Huaijin WangWang, Huaijin Ohio State UniversityChina Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps Committee Member in Program Committee within the LMPL-track
Jianrong WangWang, Jianrong Tianjin UniversityChina DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Jiawei WangWang, Jiawei UNSW Efficient Abstract Interpretation via Selective Widening
Jie WangWang, Jie Huawei Technologies Co., Ltd CG-Bench: Can Language Models Assist Call Graph Construction in the Real World?
Jingbo WangWang, Jingbo Purdue University Probabilistic Inference for Datalog with Correlated Inputs
Kailong WangWang, Kailong Huazhong University of Science and TechnologyChina Enhancing Semantic Understanding in Pointer Analysis Using Large Language Models
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
Meng WangWang, Meng University of BristolUnited Kingdom Committee Member in Program Committee within the Haskell-track
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 Reasoning as a Resource: Optimizing Fast and Slow Thinking in Code Generation Models Committee Member in Program Committee within the LMPL-track
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
Yuepeng WangWang, Yuepeng Simon Fraser UniversityCanada Committee Member in Program Committee within the SAS -track
Yuning WangWang, Yuning Rutgers University Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the ML Family Workshop-track Committee Member in Organising Committee within the TyDe-track
Zhongyi WangWang, Zhongyi Zhejiang University, ChinaChina Preguss: It Analyzes, It Specifies, It Verifies
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
Syed Waqar NabiWaqar Nabi, Syed University of Glasgow Bridging Disciplinary Gaps in Climate Research Through Programming Accessibility and Interdisciplinary Collaboration
Adam WarskiWarski, Adam SoftwareMillPoland How Functional is Direct-Style?
Kazuki WatanabeWatanabe, Kazuki National Institute of Informatics; SOKENDAIJapan A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Takuo WatanabeWatanabe, Takuo Institute of Science TokyoJapan Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search Session Chair of Research Paper 1 (part of MPLR) Co-operative JIT Compilation for Resource-Constrained Low-Power Coprocessors Committee Member in Program Committee within the MPLR-track
Yasunari WatanabeWatanabe, Yasunari AhrefsJapan Co-chair in Program Committee within the OCaml-track
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Doctoral Symposium Chair in Organizing Committee for ICFP/SPLASH 2025 Doctoral Symposium Chair in Organizing Committee for SPLASH 2025 Doctoral Symposium Chair in Organizing Committee for ICFP 2025 WebAssembly Research Tools Tutorial Session Chair of Session 2 (part of SPLASH Doctoral Symposium) Session Chair of Session 1 (part of SPLASH Doctoral Symposium) Introductions [Closed Session] Adjudication meeting for SIGPLAN's John Vlissides award Organizing Chair in Program Committee and Panel within the SPLASH Doctoral Symposium-track Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track Session Chair of Session 3 (part of WebAssembly Workshop) Session Chair of Session 1 (part of WebAssembly Workshop) Session Chair of Session 2 (part of WebAssembly Workshop) Closing Organizing Chair in Organizers within the WebAssembly Workshop-track Committee Member in Program Committee within the MPLR-track PLMW Welcome Committee Member in Program Committee within the PLMW @ ICFP/SPLASH-track
Joe WattWatt, Joe *Institute for Infocomm Research, ASTARSingapore** Student Volunteer Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for SPLASH 2025 Student Volunteer Co-Chair in Organizing Committee for ICFP 2025 Student Volunteer Chair in Organizers within the ICFP/SPLASH Volunteers-track
Tan Wei HanWei Han, Tan Local Arrangements Chair in Organizing Committee for ICFP/SPLASH 2025 Local Arrangements Chair in Organizing Committee for SPLASH 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 Mixing transformation and symbolic execution with continuation for WebAssembly 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 Committee Member in ICFP Programme Committee within the ICFP Papers-track Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse Session Chair of LLMs for Code Generation (part of LMPL) Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad Committee Member in Program Committee within the miniKanren-track Committee Member in Program Committee within the The Scala Workshop-track
Ivan WeiWei, Ivan University of Michigan Incremental Bidirectional Typing via Order Maintenance
Michele WeilandWeiland, Michele Committee Member in Program Committee within the PROPL-track
Robert WeingartWeingart, Robert Imperial College London Total Type Classes
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Committee Member in ICFP Programme Committee within the ICFP Papers-track Rebound: Efficient, expressive, and well-scoped binding
Hongbo WenWen, Hongbo University of California, Santa Barbara & Riema Labs Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Ming WenWen, Ming Huazhong University of Science and TechnologyChina Committee Member in Program Committee within the LMPL-track
Zhongzhen WenWen, Zhongzhen Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Benjamin WernerWerner, Benjamin LIX, IPP Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
Sam WestrickWestrick, Sam New York UniversityUnited States Publicity Chair in Organizing Committee for ICFP 2025 Publicity Chair in Steering Committee for ICFP 2025 Committee Member in Program Committee within the SPLASH FARM-track Session Chair of ML Workshop 2 (part of ML Family Workshop) Welcome Chair in Program Committee within the ML Family Workshop-track Committee Member in Program Committee within the OCaml-track
Leo WhiteWhite, Leo Jane StreetUnited Kingdom Modal Effect Types Committee Member in ICFP Programme Committee within the ICFP Papers-track Committee Member in Program Committee within the HOPE-track
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/SPLASH 2025 Sponsorship Co-Chair in Organizing Committee for SPLASH 2025 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
Jackson WoodruffWoodruff, Jackson University of EdinburghUnited Kingdom ScaIR: Type-safe Compiler Framework Compatible with MLIR
Chris WoodsWoods, Chris [Keynote] “Codename: Tunahead” aka Software Engineering Economics for Runtimes
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 Round table on ownership challenges Committee Member in Organizing Committee within the IWACO-track PyErlang -- a stepping stone towards behaviour-oriented concurrency in Python
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 State Key Laboratory for Novel Software Technology, Nanjing University 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
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom Total Type Classes
Rongxin WuWu, Rongxin Xiamen UniversityChina TailTracer: Continuous Tail Tracing for Production Use Committee Member in Program Committee within the LMPL-track
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 Maria XekalakiXekalaki, Maria University of Manchester, UK Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware TornadoViz: Visualizing Heterogeneous Execution Patterns in Modern Managed Runtime Systems
Li-yao XiaXia, Li-yao INRIA SaclayFrance Committee Member in Program Committee within the Haskell-track
Xin XiaXia, Xin Zhejiang UniversityChina Enhancing Software Engineering with Large Language Models: Insights, Challenges, and Future Directions
Yifan XiaXia, Yifan Beyond Static Pattern Matching? Rethinking Automatic Cryptographic API Misuse Detection in the Era of LLMs
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
Fei XieXie, Fei Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
Lihan XieXie, Lihan Shanghai Jiao Tong University The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics
Linna XieXie, Linna Nanjing UniversityChina PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
Ningning XieXie, Ningning University of TorontoCanada PLMW Co-Chair in Organizing Committee for ICFP/SPLASH 2025 Multi-stage Programming with Splice Variables Committee Member in ICFP Programme Committee within the ICFP Papers-track Session Chair of Talks (part of Haskell) Session Chair of Keynote + Research paper (part of Haskell) Chair's report Welcome Co-chair in Program Committee within the Haskell-track Smart Handlers: Handling the selection monad PLMW Welcome Committee Member in Program Committee within the PLMW @ ICFP/SPLASH-track
Ruifeng XieXie, Ruifeng Peking University Effectful Lenses: There and Back with Different Monads Compositions for Free: Reasoning about Effectful Lenses
Szumi XieXie, Szumi Eötvös Loránd University (ELTE)Hungary Session Chair of Session 2 (part of TyDe) The conatural numbers form an exponential commutative semiring
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 Compiling Quantum Circuits How to Synthesize Quantum-Circuit Optimizers Dependency-Aware Compilation for Surface Code Quantum Architectures Checking Observational Correctness of Database Systems
Baowen XuXu, Baowen Nanjing University An Empirical Study of Bugs in the rustc Compiler Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study
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 Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-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 System Capybara: Capture Tracking for Ownership and Borrowing
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 Berk YagliYagli, Berk Concert: False Awakening on a Mediterranean Island
Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk) TEAL: a Total Expressive Assembly Language Frex: Dependently Typed Algebraic Simplification
Junchi YanYan, Junchi Shanghai Jiao Tong University The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics
Yanyan YanYan, Yanyan Nanjing UniversityChina Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study
Zhenyu YanYan, Zhenyu Peking UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Hongseok YangYang, Hongseok KAISTRepublic of Korea On the Structure of Abstract Interpreters Programme Committee in Program Committee within the OlivierFest-track
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
Mingqi YangYang, Mingqi Zhejiang University Preguss: It Analyzes, It Specifies, It Verifies
Sen YangYang, Sen Yale University Agora: Trust Less and Open More in Verification for Confidential Computing
Shengyuan YangYang, Shengyuan University of Wisconsin-Madison Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
Yafei YangYang, Yafei Indiana University Committing to the bit: Relational programming with semiring arrays and SAT solving
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
Zhixuan YangYang, Zhixuan Imperial College LondonUnited Kingdom Committee Member in Program Committee within the TyDe-track
Zhou YangYang, Zhou University of Alberta, Alberta Machine Intelligence Institute Canada Committee Member in Program Committee within the LMPL-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 Bounded-Exhaustive Subspace Diversification for SMT Solver Testing Committee Member in Program Committee within the SAS -track Committee Member in Program Committee within the LMPL-track
Shunyu YaoYao, Shunyu Virginia Tech Memory Tiering in Python Virtual Machine
Yuan YaoYao, Yuan Nanjing UniversityChina Committee Member in Program Committee within the LMPL-track
Chengfeng YeYe, Chengfeng The Hong Kong University of Science and TechnologyChina ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection
He YeYe, He Carnegie Mellon University Committee Member in Organizing Committee within the LMPL-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
Jooyong YiYi, Jooyong UNISTSouth Korea Committee Member in Program Committee within the SAS -track
Kwangkeun YiYi, Kwangkeun Seoul National University React-tRace: A Semantics for Understanding React Hooks
Xiao YiYi, Xiao The Chinese University of Hong Kong Preguss: It Analyzes, It Specifies, It Verifies
Jianwei YinYin, Jianwei Zhejiang UniversityChina Preguss: It Analyzes, It Specifies, It Verifies
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
James YouYou, James University of WaterlooCanada Taking away Mutation
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
Jeffrey YoungYoung, Jeffrey Epic Games United States Session Chair of FUNARCH Talks #2 (part of FUNARCH) Session Chair of FUNARCH Talks #1 (part of FUNARCH) Lightning Talks Program Chair in Program Committee within the FUNARCH-track
Neringa YoungYoung, Neringa Lithuania SIGPLAN Conference Manager in Organizing Committee for ICFP/SPLASH 2025 SIGPLAN Conference Manager in Organizing Committee for SPLASH 2025 SIGPLAN Conference Manager in Organizing Committee for ICFP 2025
Robin YoungYoung, Robin University of Cambridge Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings Challenges in Practice: Building a Usable Library for Planetary-Scale Embeddings
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
Ting YuanYuan, Ting CG-Bench: Can Language Models Assist Call Graph Construction in the Real World?
Yongwei YuanYuan, Yongwei Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track
Yuanyuan YuanYuan, Yuanyuan ETH Zurich Committee Member in Program Committee within the LMPL-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
Tom YuvilerYuviler, Tom Technion Enhancing Neural Network Robustness via Synthesis of Repair Programs
Z Enea ZaffanellaZaffanella, Enea University of ParmaItaly Committee Member in Program Committee within the SAS -track
Matei ZahariaZaharia, Matei UC Berkeley Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad
Foivos S. ZakkakZakkak, Foivos S. Red HatGreece MaTSa: Race Detection in Java SmartSweep: Efficient Space Reclamation in Tiered Managed Heaps
Yannick ZakowskiZakowski, Yannick InriaFrance Structural temporal logic for mechanized program verification Committee Member in OOPSLA Review Committee within the SPLASH OOPSLA-track
Giacomo ZanattaZanatta, Giacomo Ca’ Foscari University of VeniceItaly Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-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
Jun ZengZeng, Jun Chongqing UniversityChina Challenges in C++ to Rust Translation with Large Language Models: A Preliminary Empirical Study
Stefan ZetzscheZetzsche, Stefan AmazonUnited Kingdom Committee Member in Artifact Evaluation Committee within the SPLASH OOPSLA Artifacts-track Committee Member in Artifact Evaluation Committe within the ICFP 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
Tianyu ZhanZhan, Tianyu Virginia Tech Memory Tiering in Python Virtual Machine
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 SPLASH General Chair in Organizing Committee for ICFP/SPLASH 2025 Steering Committee Member in Steering Committee for SPLASH 2025 General Chair in Organizing Committee for SPLASH 2025 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 ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection Organizer in Organizing Committee within the Sponsor Invited Talks-track
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
Haiquan ZhangZhang, Haiquan Tencent Security Yunding Lab Improving SAST Detection Capability with LLMs and Enhanced DFA
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 Poster Co-Chair in Organizing Committee for SPLASH 2025 Fast Constraint Synthesis for C++ Function Templates Chair in Organizing Committee within the SPLASH Posters-track From Within: Compiler Testing and Validation via Compilers Committee Member in Program Committee within the SAS -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
Song ZhangZhang, Song None Derive class instances topdown and derive ttg automatically
Teng ZhangZhang, Teng Nanjing UniversityChina Committee Member in SAS Artifact Evaluation Committee within the SAS Artifact-track
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
Tianyi ZhangZhang, Tianyi Purdue UniversityUnited States Committee Member in Program Committee within the HATRA-track
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
Wenrui ZhangZhang, Wenrui Huawei Technologies Co., Ltd CG-Bench: Can Language Models Assist Call Graph Construction in the Real World?
Wuqi ZhangZhang, Wuqi MegaETHHong Kong SAR China Committee Member in Program Committee within the LMPL-track
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 Committee Member in Program Committee within the SAS -track
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 Zero-Overhead Lexical Effect Handlers Compiling with Generating Functions Committee Member in Program Committee within the HOPE-track
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 Technology A Sound Static Analysis Approach to I/O API Migration
Zhuo ZhangZhang, Zhuo Columbia UniversityUnited States Session Chair of LLMs for Program Analysis and Verification II (part of LMPL) Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis Committee Member in Organizing Committee within the LMPL-track
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
Yaoyu ZhaoZhao, Yaoyu EPFL, LAMPSwitzerland Migrating Large-scale Scala Projects to Explicit-nulls with the Help from LLMs
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
Junda ZhengZheng, Junda Bounded-Exhaustive Subspace Diversification for SMT Solver Testing
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 Range-Analysis-Based Optimization for SML/NJ Committee Member in Artifact Evaluation Committe within the ICFP Artifacts-track
Dinghong ZhongZhong, Dinghong Tufts University Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse
Si Cheng ZhongZhong, Si Cheng University of Toronto Toward Repository-Level Program Verification with Large Language Models
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
Anshunkang ZhouZhou, Anshunkang The Hong Kong University of Science and TechnologyChina ClearAgent: Agentic Binary Analysis for Effective Vulnerability Detection
Chenyu ZhouZhou, Chenyu University of Southern CaliforniaUnited States Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Diyu ZhouZhou, Diyu Peking University A Sound Static Analysis Approach to I/O API Migration
Dizhi ZhouZhou, Dizhi Committee Member in Program Committee within the LMPL-track
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
Andrea ZitoZito, Andrea University of Torino, Italy A typed approach to ontology manipulation (experience report)
Yoni ZoharZohar, Yoni Bar Ilan UniversityUnited States Lessons from Building a Hardware Compiler in Scala 3: A Practitioner Perspective
Li ZongjieZongjie, Li Hong Kong University of Science and TechnologyChina API-guided Dataset Synthesis to Finetune Large Code Models
Philip ZuckerZucker, Philip DraperUnited States Committee Member in Program Committee within the miniKanren-track
Damien ZuffereyZufferey, Damien SonarSourceSwitzerland Characterizing Implementability of Global Protocols with Infinite States and Data
Tianyu ZuoZuo, Tianyu CCB Fintech Co., Ltd. Dynamic and Static Code Analysis for Java Programs on Heterogeneous Hardware
Zhiqiang ZuoZuo, Zhiqiang Nanjing UniversityChina HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming TailTracer: Continuous Tail Tracing for Production Use Live Program Analysis for Security-Critical Scenarios
Aron ZwaanZwaan, Aron Delft University of TechnologyNetherlands Language-Parametric Reference Synthesis
Andrés C. Zúñiga-GonzálezZúñiga-González, Andrés C. University of Cambridge Scaling the Urban Forest: An Integrated Framework for Managing Cities by Fusing Raster and Vector Data
Å Beatrice ÅkerblomÅkerblom, Beatrice Stockholm University Committee Member in Program Committee within the MPLR-track
É Gergő ÉrdiÉrdi, Gergő Standard Chartered BankSingapore Session Chair of Language design (part of Haskell) A Clash Course in Solving Sudoku (Functional Pearl) Committee Member in Program Committee within the Haskell-track
Š Artjoms ŠinkarovsŠinkarovs, Artjoms University of Southampton Correctness Meets Performance: From Agda to Futhark Committee Member in Program Committee within the ICFP Student Research Competition-track

ICFP/SPLASH 2025 Contributors

Results (1913)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia