ACM SIGPLAN International Conference on Functional Programming, ICFP 2016


Title/Authors Title Research Artifacts
[?] A research artifact is any by-product of a research project that is not directly included in the published research paper. In Computer Science research this is often source code and data sets, but it could also be media, documentation, inputs to proof assistants, shell-scripts to run experiments, etc.
Details

The best of both worlds: linear functional programming without compromise

J. Garrett Morris

The best of both worlds: linear functional programming without compromise

Details
Discussion Comments: 0
Verification: Author has not verified information

Compact bit encoding schemes for simply-typed lambda-terms

Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Compact bit encoding schemes for simply-typed lambda-terms

Details
Discussion Comments: 0
Verification: Authors have not verified information

A functional programmer's guide to homotopy type theory

Dan Licata

A functional programmer's guide to homotopy type theory

Details
Discussion Comments: 0
Verification: Author has not verified information

Refinement through restraint: bringing down the cost of verification

Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein

Refinement through restraint: bringing down the cost of verification

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

A type theory for incremental computational complexity with control flow changes

Ezgi Çiçek, Zoe Paraskevopoulou, Deepak Garg

A type theory for incremental computational complexity with control flow changes

Details
Discussion Comments: 0
Verification: Authors have not verified information

Ghostbuster: a tool for simplifying and converting GADTs

Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, Ryan R. Newton

Ghostbuster: a tool for simplifying and converting GADTs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Deriving a probability density calculator (functional pearl)

Wazim Mohammed Ismail, Chung-chieh Shan

Deriving a probability density calculator (functional pearl)

Details
Discussion Comments: 0
Verification: Authors have not verified information

Disjoint intersection types

Bruno C. d. S. Oliveira, Zhiyuan Shi, João Alpuim

Disjoint intersection types

Details
Discussion Comments: 0
Verification: Authors have not verified information

A glimpse of Hopjs

Manuel Serrano, Vincent Prunet

A glimpse of Hopjs

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

A fully concurrent garbage collector for functional programs on multicore processors

Katsuhiro Ueno, Atsushi Ohori

A fully concurrent garbage collector for functional programs on multicore processors

Details
Discussion Comments: 0
Verification: Authors have not verified information

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

David Darais, David Van Horn

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

Details
Discussion Comments: 0
Verification: Authors have not verified information

Elaborator reflection: extending Idris in Idris

David R. Christiansen, Edwin Brady

Elaborator reflection: extending Idris in Idris

Details
Discussion Comments: 0
Verification: Authors have not verified information

Oh Lord, please don't let contracts be misunderstood (functional pearl)

Christos Dimoulas, Max S. New, Robert Bruce Findler, Matthias Felleisen

Oh Lord, please don't let contracts be misunderstood (functional pearl)

Details
Discussion Comments: 0
Verification: Authors have not verified information

Sequent calculus as a compiler intermediate language

Paul Downen, Luke Maurer, Zena M. Ariola, Simon Peyton Jones

Sequent calculus as a compiler intermediate language

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Queueing and glueing for optimal partitioning (functional pearl)

Shin-Cheng Mu, Yu-Hsi Chiang, Yu-Han Lyu

Queueing and glueing for optimal partitioning (functional pearl)

Details
Discussion Comments: 0
Verification: Authors have not verified information

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

Eric L. Seidel, Ranjit Jhala, Westley Weimer

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing

Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki

Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing

Details
Discussion Comments: 0
Verification: Authors have not verified information

Higher-order ghost state

Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Higher-order ghost state

Details
Discussion Comments: 0
Verification: Authors have not verified information

All sorts of permutations (functional pearl)

Jan Christiansen, Nikita Danilenko, Sandra Dylus

All sorts of permutations (functional pearl)

Details
Discussion Comments: 0
Verification: Authors have not verified information

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

David Castro, Kevin Hammond, Susmit Sarkar

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

Details
Discussion Comments: 0
Verification: Authors have not verified information

Partial type equivalences for verified dependent interoperability

Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter

Partial type equivalences for verified dependent interoperability

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

An abstract memory functor for verified C static analyzers

Sandrine Blazy, Vincent Laporte, David Pichardie

An abstract memory functor for verified C static analyzers

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis

Thomas Gilray, Michael D. Adams, Matthew Might

Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis

Details
Discussion Comments: 0
Verification: Authors have not verified information

A lambda-calculus foundation for universal probabilistic programming

Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak

A lambda-calculus foundation for universal probabilistic programming

Details
Discussion Comments: 0
Verification: Authors have not verified information

A new verified compiler backend for CakeML

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

A new verified compiler backend for CakeML

Details
Discussion Comments: 0
Verification: Authors have not verified information

Indexed codata types

David Thibodeau, Andrew Cave, Brigitte Pientka

Indexed codata types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Fully abstract compilation via universal embedding

Max S. New, William J. Bowman, Amal Ahmed

Fully abstract compilation via universal embedding

Details
Discussion Comments: 0
Verification: Authors have not verified information

Hierarchical memory management for parallel programs

Ram Raghunathan, Stefan K. Muller, Umut A. Acar, Guy E. Blelloch

Hierarchical memory management for parallel programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

String diagrams for free monads (functional pearl)

Maciej Piróg, Nicolas Wu

String diagrams for free monads (functional pearl)

Details
Discussion Comments: 0
Verification: Authors have not verified information

Talking bananas: structural recursion for session types

Sam Lindley, J. Garrett Morris

Talking bananas: structural recursion for session types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Unifiers as equivalences: proof-relevant unification of dependently typed data

Jesper Cockx, Dominique Devriese, Frank Piessens

Unifiers as equivalences: proof-relevant unification of dependently typed data

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Datafun: a functional Datalog

Michael Arntzenius, Neelakantan R. Krishnaswami

Datafun: a functional Datalog

Details
Discussion Comments: 0
Verification: Authors have not verified information

TensorFlow: learning functions at scale

Martín Abadi

TensorFlow: learning functions at scale

Details
Discussion Comments: 0
Verification: Author has not verified information

Dag-calculus: a calculus for parallel computation

Umut A. Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski

Dag-calculus: a calculus for parallel computation

Details
Discussion Comments: 0
Verification: Authors have not verified information

Automatically disproving fair termination of higher-order functional programs

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Automatically disproving fair termination of higher-order functional programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Context-free session types

Peter Thiemann, Vasco T. Vasconcelos

Context-free session types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Set-theoretic types for polymorphic variants

Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyen

Set-theoretic types for polymorphic variants

Details
Discussion Comments: 0
Verification: Authors have not verified information

Journey to find bugs in JavaScript web applications in the wild

Sukyoung Ryu

Journey to find bugs in JavaScript web applications in the wild

Details
Discussion Comments: 0
Verification: Author has not verified information

Combining effects and coeffects via grading

Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, Tarmo Uustalu

Combining effects and coeffects via grading

Details
Discussion Comments: 0
Verification: Authors have not verified information

Experience report: growing and shrinking polygons for random testing of computational geometry algorithms

Ilya Sergey

Experience report: growing and shrinking polygons for random testing of computational geometry algorithms

Details
Discussion Comments: 0
Verification: Author has not verified information