ICFP 2020

37 papers

1. A dependently typed calculus with pattern matching and erasure inference · Matus Tejiscak
2. A general approach to define binders using matching logic · Xiaohong Chen, Grigore Rosu
3. A quick look at impredicativity · Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis
4. A unified view of modalities in type systems · Andreas Abel, Jean-Philippe Bernardy
5. Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies · Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, Michel Steuwer
6. Compiling effect handlers in capability-passing style · Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann
7. Composing and decomposing op-based CRDTs with semidirect products · Matthew Weidner, Heather Miller, Christopher Meiklejohn
8. Computation focusing · Nick Rioux, Steve Zdancewic
9. Cosmo: a concurrent separation logic for multicore OCaml · Glen Mével, Jacques-Henri Jourdan, François Pottier
10. Denotational recurrence extraction for amortized analysis · Joseph W. Cutler, Daniel R. Licata, Norman Danner
11. Duplo: a framework for OCaml post-link optimisation · Nándor Licker, Timothy M. Jones
12. Effect handlers, evidently · Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen
13. Effects for efficiency: asymptotic speedup with first-class control · Daniel Hillerström, Sam Lindley, John Longley
14. Elaboration with first-class implicit function types · András Kovács
15. Higher-order demand-driven symbolic evaluation · Zachary Palmer, Theodore Park, Scott F. Smith, Shiwei Weng
16. Kindly bent to free us · Gabriel Radanne, Hannes Saffrich, Peter Thiemann
17. Kinds are calling conventions · Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg
18. Liquid information flow control · Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama
19. Liquid resource types · Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, Nadia Polikarpova
20. Lower your guards: a compositional pattern-match coverage checker · Sebastian Graf, Simon Peyton Jones, Ryan G. Scott
21. Parsing with zippers (functional pearl) · Pierce Darragh, Michael D. Adams
22. Program sketching with live bidirectional evaluation · Justin Lubin, Nick Collins, Cyrus Omar, Ravi Chugh
23. Raising expectations: automating expected cost analysis with types · Di Wang, David M. Kahn, Jan Hoffmann
24. Recovering purity with comonads and capabilities · Vikraman Choudhury, Neel Krishnaswami
25. Regular language type inference with term rewriting · Timothée Haudebourg, Thomas Genet, Thomas P. Jensen
26. Retrofitting parallelism onto OCaml · K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo + 3 more
27. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris · Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
28. Sealing pointer-based optimizations behind pure functions · Daniel Selsam, Simon Hudon, Leonardo de Moura
29. Separation logic for sequential programs (functional pearl) · Arthur Charguéraud
30. Signature restriction for polymorphic algebraic effects · Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
31. Sparcl: a language for partially-invertible computation · Kazutaka Matsuda, Meng Wang
32. Stable relations and abstract interpretation of higher-order programs · Benoît Montagu, Thomas P. Jensen
33. Staged selective parser combinators · Jamie Willis, Nicolas Wu, Matthew Pickering
34. SteelCore: an extensible concurrent separation logic for effectful dependently typed programs · Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
35. Strong functional pearl: Harper's regular-expression matcher in Cedille · Aaron Stump, Christopher Jenkins, Stephan Spahn, Colin McDonald
36. TLC: temporal logic of distributed components · Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin
37. The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl) · Lionel Parreaux