Venues / ICFP /

ICFP 2017

44 papers

A framework for adaptive differential privacy · Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, Benjamin C. Pierce
A metaprogramming framework for formal verification · Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
A pretty but not greedy printer (functional pearl) · Jean-Philippe Bernardy
A relational logic for higher-order programs · Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
A specification for dependent types in Haskell · Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, Richard A. Eisenberg
A unified approach to solving seven programming problems (functional pearl) · William E. Byrd, A. Ballantyne, Gregory Rosenblatt, Matthew Might
Abstracting definitional interpreters (functional pearl) · David Darais, Nicholas Labich, Phuc C. Nguyen, David Van Horn
Automating sized-type inference for complexity analysis · Martin Avanzini, Ugo Dal Lago
Better living through operational semantics: an optimizing compiler for radio protocols · Geoffrey Mainland
Chaperone contracts for higher-order sessions · Hernán C. Melgratti, Luca Padovani
Compiling to categories · Conal Elliott
Constrained type families · J. Garrett Morris, Richard A. Eisenberg
Effect-driven QuickChecking of compilers · Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson
Faster coroutine pipelines · J. Michael Spivey
Foundations of strong call by need · Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, Delia Kesner
Generic functional parallel algorithms: scan and FFT · Conal Elliott
Gradual session types · Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, Philip Wadler
Gradual typing with union and intersection types · Giuseppe Castagna, Victor Lanvin
Herbarium Racketensis: a stroll through the woods (functional pearl) · Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Robert Bruce Findler
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation · Makoto Hamana
Imperative functional programs that explain their work · Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney
Inferring scope through syntactic sugar · Justin Pombrio, Shriram Krishnamurthi, Mitchell Wand
Kami: a platform for high-level parametric hardware specification and its modular verification · Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind
Local refinement typing · Benjamin Cosman, Ranjit Jhala
Lock-step simulation is child's play (experience report) · Joachim Breitner, Chris Smith
Manifest sharing with session types · Stephanie Balzer, Frank Pfenning
No-brainer CPS conversion (functional pearl) · Milo Davis, William Meehan, Olin Shivers
Normalization by evaluation for sized dependent types · Andreas Abel, Andrea Vezzosi, Théo Winterhalter
On polymorphic gradual typing · Yuu Igarashi, Taro Sekiyama, Atsushi Igarashi
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control · Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
Parametric quantifiers for dependent type theory · Andreas Nuyts, Andrea Vezzosi, Dominique Devriese
Persistence for the masses: RRB-vectors in a systems language · Juan Pedro Bolívar Puente
Prototyping a query compiler using Coq (experience report) · Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jérôme Siméon
Scaling up functional programming education: under the hood of the OCaml MOOC · Benjamin Canou, Roberto Di Cosmo, Grégoire Henry
SpaceSearch: a library for building and verifying solver-aided tools · Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
Staged generic programming · Jeremy Yallop
Super 8 languages for making movies (functional pearl) · Leif Andersen, Stephen Chang, Matthias Felleisen
Symbolic conditioning of arrays in probabilistic programs · Praveen Narayanan, Chung-chieh Shan
Testing and debugging functional reactive programming · Ivan Perez, Henrik Nilsson
Theorems for free for free: parametricity, with and without types · Amal Ahmed, Dustin Jamner, Jeremy G. Siek, Philip Wadler
Verified low-level programming embedded in F · Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin + 5 more
Verifying efficient function calls in CakeML · Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
Visitors unchained · François Pottier
Whip: higher-order contracts for modern services · Lucas Waye, Stephen Chong, Christos Dimoulas