ICFP – Journal Issue

Artifacts Reusable Article: icfp22main-p1-p doi:10.1145/3547621

Searching Entangled Program Spaces
James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, and Nadia Polikarpova
(Massachusetts Institute of Technology, USA; University of California at San Diego, USA; Well-Typed LLP, UK)

Artifacts Reusable Article: icfp22main-p3-p doi:10.1145/3547622

Generating Circuits with Generators
Marek Materzok
(University of Wrocław, Poland)

Artifacts Reusable Article: icfp22main-p7-p doi:10.1145/3549821

Monadic Compiler Calculation (Functional Pearl)
Patrick Bahr and Graham Hutton
(IT University of Copenhagen, Denmark; University of Nottingham, UK)

Artifacts Reusable Article: icfp22main-p10-p doi:10.1145/3547624

A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine
Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab
(University of Wrocław, Poland)

Artifacts Reusable Article: icfp22main-p14-p doi:10.1145/3549822

Linearly Qualified Types: Generic Inference for Capabilities and Uniqueness
Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg
(Tweag, France; Imperial College London, UK; University of Gothenburg, Sweden)

Publisher's Version Article: icfp22main-p15-p doi:10.1145/3547626

Propositional Equality for Gradual Dependently Typed Programming
Joseph Eremondi, Ronald Garcia, and Éric Tanter
(University of British Columbia, Canada; University of Chile, Chile)

Publisher's Version Article: icfp22main-p16-p doi:10.1145/3547627

Verified Symbolic Execution with Kripke Specification Monads (and No Meta-programming)
Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, and Dominique Devriese
(Vrije Universiteit Brussel, Belgium; Newcastle University, UK; KU Leuven, Belgium)

Artifacts Reusable Article: icfp22main-p17-p doi:10.1145/3547628

Datatype-Generic Programming Meets Elaborator Reflection
Hsiang-Shang Ko, Liang-Ting Chen, and Tzu-Chi Lin
(Academia Sinica, Taiwan)

Artifacts Reusable Article: icfp22main-p20-p doi:10.1145/3547629

Formal Reasoning about Layered Monadic Interpreters
Irene Yoon, Yannick Zakowski, and Steve Zdancewic
(University of Pennsylvania, USA; Inria, France)

Artifacts Reusable Article: icfp22main-p21-p doi:10.1145/3547630

Later Credits: Resourceful Reasoning for the Later Modality
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer
(MPI-SWS, Germany; New York University, USA; Massachusetts Institute of Technology, USA; Radboud University Nijmegen, Netherlands; Aarhus University, Denmark)

Artifacts Reusable Article: icfp22main-p23-p doi:10.1145/3547631

Program Adverbs and Tlön Embeddings
Yao Li and Stephanie Weirich
(Portland State University, USA; University of Pennsylvania, USA)

Artifacts Reusable Article: icfp22main-p26-p doi:10.1145/3547632

Structural versus Pipeline Composition of Higher-Order Functions (Experience Report)
Elijah Rivera and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Article: icfp22main-p36-p doi:10.1145/3547633

Reference Counting with Frame Limited Reuse
Anton Lorenzen and Daan Leijen
(University of Bonn, Germany; Microsoft Research, USA)

Artifacts Reusable Article: icfp22main-p41-p doi:10.1145/3547634

Modular Probabilistic Models via Algebraic Effects
Minh Nguyen, Roly Perera, Meng Wang, and Nicolas Wu
(University of Bristol, UK; Alan Turing Institute, UK; Imperial College London, UK)

Artifacts Reusable Article: icfp22main-p42-p doi:10.1145/3547635

A Completely Unique Account of Enumeration
Cas van der Rest and Wouter Swierstra
(Delft University of Technology, Netherlands; Utrecht University, Netherlands)

Publisher's Version Article: icfp22main-p44-p doi:10.1145/3547636

Introduction and Elimination, Left and Right
Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen
(University of Tübingen, Germany; University of Massachusetts at Lowell, USA)

Artifacts Reusable Article: icfp22main-p45-p doi:10.1145/3547637

Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom
Jules Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)

Artifacts Reusable Article: icfp22main-p48-p doi:10.1145/3547638

Fusing Industry and Academia at GitHub (Experience Report)
Patrick Thomson, Rob Rix, Nicolas Wu, and Tom Schrijvers
(GitHub, USA; GitHub, Canada; Imperial College London, UK; KU Leuven, Belgium)

Publisher's Version Article: icfp22main-p49-p doi:10.1145/3547639

‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)
Sebastian Ullrich and Leonardo de Moura
(KIT, Germany; Microsoft Research, USA)

Artifacts Reusable Article: icfp22main-p50-p doi:10.1145/3547640

Staged Compilation with Two-Level Type Theory
András Kovács
(Eötvös Loránd University, Hungary)

Artifacts Reusable Article: icfp22main-p52-p doi:10.1145/3547641

Constraint-Based Type Inference for FreezeML
Frank Emrich, Jan Stolarek, James Cheney, and Sam Lindley
(University of Edinburgh, UK)

Publisher's Version Article: icfp22main-p53-p doi:10.1145/3547642

Safe Couplings: Coupled Refinement Types
Elizaveta Vasilenko, Niki Vazou, and Gilles Barthe
(IMDEA Software Institute, Spain; HSE University, Russia; MPI-SP, Germany)

Artifacts Reusable Article: icfp22main-p58-p doi:10.1145/3547643

Practical Generic Programming over a Universe of Native Datatypes
Lucas Escot and Jesper Cockx
(Delft University of Technology, Netherlands)

Artifacts Reusable Article: icfp22main-p66-p doi:10.1145/3547644

Analyzing Binding Extent in 3CPS
Benjamin Quiring, John Reppy, and Olin Shivers
(University of Maryland, USA; University of Chicago, USA; Northeastern University, USA)

Artifacts Reusable Article: icfp22main-p70-p doi:10.1145/3547645

Entanglement Detection with Near-Zero Cost
Sam Westrick, Jatin Arora, and Umut A. Acar
(Carnegie Mellon University, USA)

Archive submitted (490 kB)

Artifacts Reusable Article: icfp22main-p75-p doi:10.1145/3547646

Aeneas: Rust Verification by Functional Translation
Son Ho and Jonathan Protzenko
(Inria, France; Microsoft Research, USA)

Artifacts Reusable Article: icfp22main-p82-p doi:10.1145/3547647

Automatically Deriving Control-Flow Graph Generators from Operational Semantics
James Koppel, Jackson Kearl, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)

Artifacts Reusable Article: icfp22main-p85-p doi:10.1145/3547648

Normalization for Fitch-Style Modal Calculi
Nachiappan Valliappan, Fabian Ruch, and Carlos Tomé Cortiñas
(Chalmers University of Technology, Sweden)

Artifacts Reusable Article: icfp22main-p88-p doi:10.1145/3547649

Multi Types and Reasonable Space
Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni
(Inria, France; École Polytechnique, France; University of Bologna, Italy)

Publisher's Version Article: icfp22main-p89-p doi:10.1145/3547650

On Feller Continuity and Full Abstraction
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo
(MPI-SP, Germany; IMDEA Software Institute, Spain; CNRS, France; University of Bologna, Italy; Inria, France)

Publisher's Version Article: icfp22main-p91-p doi:10.1145/3547651

The Theory of Call-by-Value Solvability
Beniamino Accattoli and Giulio Guerrieri
(Inria, France; École Polytechnique, France; Huawei Edinburgh Research Centre, UK)

Publisher's Version Article: icfp22main-p92-p doi:10.1145/3547652

Random Testing of a Higher-Order Blockchain Language (Experience Report)
Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey
(National University of Singapore, Singapore; Zilliqa Research, Russia; University of Maryland at College Park, USA)

Artifacts Reusable Article: icfp22main-p102-p doi:10.1145/3547653

Flexible Presentations of Graded Monads
Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu
(National Institute of Informatics, Japan; Reykjavik University, Iceland; Tallinn University of Technology, Estonia; Imperial College London, UK)

Publisher's Version Article: icfp22main-p104-p doi:10.1145/3547654

A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, and Éric Tanter
(Inria, France; University of Chile, Chile)