ICFP 2021

35 papers

1. A theory of higher-order subtyping with type intervals · Sandro Stucki, Paolo G. Giarrusso
2. Algebras for weighted search · Donnacha Oisín Kidney, Nicolas Wu
3. An existential crisis resolved: type inference for first-class existential types · Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, Daniel Lee
4. An order-aware dataflow model for parallel Unix pipelines · Shivam Handa, Konstantinos Kallas, Nikos Vasilakis, Martin C. Rinard
5. Automatic amortized resource analysis with the Quantum physicist's method · David M. Kahn, Jan Hoffmann
6. CPS transformation with affine types for call-by-value implicit polymorphism · Taro Sekiyama, Takeshi Tsukada
7. Calculating dependently-typed compilers (functional pearl) · Mitchell Pickard, Graham Hutton
8. Catala: a programming language for the law · Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
9. Certifying the synthesis of heap-manipulating programs · Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey
10. Client-server sessions in linear logic · Zesen Qian, G. A. Kavvos, Lars Birkedal
11. Compositional optimizations for CertiCoq · Zoe Paraskevopoulou, John M. Li, Andrew W. Appel
12. Contextual modal types for algebraic effects and handlers · Nikita Zyuzin, Aleksandar Nanevski
13. Deriving efficient program transformations from rewrite rules · John M. Li, Andrew W. Appel
14. Distributing intersection and union types with splits and duality (functional pearl) · Xuejing Huang, Bruno C. d. S. Oliveira
15. Efficient tree-traversals: reconciling parallelism and dense data representations · Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni, Ryan R. Newton
16. Formal verification of a concurrent bounded queue in a weak memory model · Glen Mével, Jacques-Henri Jourdan
17. Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C · Ningning Xie, Daan Leijen
18. Getting to the point: index sets and parallelism-preserving autodiff for pointful array programming · Adam Paszke, Daniel D. Johnson, David Duvenaud, Dimitrios Vytiniotis, Alexey Radul, Matthew J. Johnson + 2 more
19. GhostCell: separating permissions from data in Rust · Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer
20. Grafs: declarative graph analytics · Farzin Houshmand, Mohsen Lesani, Keval Vora
21. Higher-order probabilistic adversarial computations: categorical semantics and program logics · Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
22. How to evaluate blame for gradual types · Lukas Lazarek, Ben Greenman, Matthias Felleisen, Christos Dimoulas
23. Modular, compositional, and executable formal semantics for LLVM IR · Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic
24. Newly-single and loving it: improving higher-order must-alias analysis with heap fragments · Kimball Germane, Jay McCarthy
25. Of JavaScript AOT compilation performance · Manuel Serrano
26. On continuation-passing transformations and expected cost analysis · Martin Avanzini, Gilles Barthe, Ugo Dal Lago
27. Persistent software transactional memory in Haskell · Nicolas Krauter, Patrick Raaf, Peter Braam, Reza Salkhordeh, Sebastian Erdweg, André Brinkmann
28. ProbNV: probabilistic verification of network control planes · Nick Giannarakis, Alexandra Silva, David Walker
29. Propositions-as-types and shared state · Pedro Rocha, Luís Caires
30. Reasoning about effect interaction by fusion · Zhixuan Yang, Nicolas Wu
31. Reasoning about the garden of forking paths · Yao Li, Li-yao Xia, Stephanie Weirich
32. Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) · Adam Chlipala
33. Steel: proof-oriented programming in a dependently typed concurrent separation logic · Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux + 1 more
34. Symbolic and automatic differentiation of languages · Conal Elliott
35. Theorems for free from separation logic specifications · Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos