| 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
|
|
Bruno C. d. S. Oliveira, Zhiyuan Shi, João Alpuim |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Manuel Serrano, Vincent Prunet |
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
|
|
|
Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, Hideya Iwasaki |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer |
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
|
|
David Castro, Kevin Hammond, Susmit Sarkar |
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
|
|
|
David Thibodeau, Andrew Cave, Brigitte Pientka |
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
|
|
|
Michael Arntzenius, Neelakantan R. Krishnaswami |
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
|
|
|
Peter Thiemann, Vasco T. Vasconcelos |
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
|
|
Ilya Sergey |
Details |
Discussion Comments:
0
Verification:
Author has
not verified
information
|