ICFP 2017 – Author Index

A B C D E F G H I J K L M N O P R S T U V W Y Z

	Abel, Andreas	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Normalization by Evaluation ..." Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France) Artifacts Reusable Article: icfp17main-main84-p (type: Full Paper) doi:
	Aguirre, Alejandro	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Relational Logic for Higher-Order ..." A Relational Logic for Higher-Order Programs Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub (IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France) Artifacts Functional Article: icfp17main-main81-p (type: Full Paper) doi:
	Ahmed, Amal	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Theorems for Free for Free: ..." Theorems for Free for Free: Parametricity, With and Without Types Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler (Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main102-p (type: Full Paper) doi:
	Andersen, Leif	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Super 8 Languages for Making ..." Super 8 Languages for Making Movies (Functional Pearl) Leif Andersen, Stephen Chang, and Matthias Felleisen (Northeastern University, USA) Artifacts Reusable Article: icfp17main-main93-p (type: Full Paper) doi:
	Arvind	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Kami: A Platform for High-Level ..." Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind (Massachusetts Institute of Technology, USA) Artifacts Functional Article: icfp17main-main16-p (type: Full Paper) doi:
	Auerbach, Joshua S.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Prototyping a Query Compiler ..." Prototyping a Query Compiler using Coq (Experience Report) Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon (IBM Research, USA) Artifacts Functional Article: icfp17main-main75-p (type: Full Paper (12 pages of text + references)) doi:
	Avanzini, Martin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Automating Sized-Type Inference ..." Automating Sized-Type Inference for Complexity Analysis Martin Avanzini and Ugo Dal Lago (University of Innsbruck, Austria; University of Bologna, Italy; Inria, France) Article: icfp17main-main32-p (type: Full Paper) doi:
	Avigad, Jeremy	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Metaprogramming Framework ..." A Metaprogramming Framework for Formal Verification Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura (Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA) Artifacts Reusable Article: icfp17main-main19-p (type: Full Paper) doi:
	Balabonski, Thibaut	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Foundations of Strong Call ..." Foundations of Strong Call by Need Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner (LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina; Stevens Institute of Technology, USA) Article: icfp17main-main65-p (type: Full Paper) doi:
	Ballantyne, Michael	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Unified Approach to Solving ..." A Unified Approach to Solving Seven Programming Problems (Functional Pearl) William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might (University of Utah, USA) Artifacts Reusable Article: icfp17main-main35-p (type: Full Paper) doi:
	Balzer, Stephanie	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Manifest Sharing with Session ..." Manifest Sharing with Session Types Stephanie Balzer and Frank Pfenning (Carnegie Mellon University, USA) Article: icfp17main-main85-p (type: Full Paper) doi:
	Barenbaum, Pablo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Foundations of Strong Call ..." Foundations of Strong Call by Need Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner (LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina; Stevens Institute of Technology, USA) Article: icfp17main-main65-p (type: Full Paper) doi:
	Barthe, Gilles	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Relational Logic for Higher-Order ..." A Relational Logic for Higher-Order Programs Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub (IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France) Artifacts Functional Article: icfp17main-main81-p (type: Full Paper) doi:
	Bernardy, Jean-Philippe	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Pretty But Not Greedy Printer ..." A Pretty But Not Greedy Printer (Functional Pearl) Jean-Philippe Bernardy (University of Gothenburg, Sweden) Article: icfp17main-main1-p (type: Full Paper) doi:
	Bhargavan, Karthikeyan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Bonelli, Eduardo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Foundations of Strong Call ..." Foundations of Strong Call by Need Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner (LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina; Stevens Institute of Technology, USA) Article: icfp17main-main65-p (type: Full Paper) doi:
	Breitner, Joachim	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Lock-Step Simulation Is Child's ..." Lock-Step Simulation Is Child's Play (Experience Report) Joachim Breitner and Chris Smith (University of Pennsylvania, USA; Google, USA) Artifacts Functional Article: icfp17main-main24-p (type: Full Paper) doi:
	Byrd, William E.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Unified Approach to Solving ..." A Unified Approach to Solving Seven Programming Problems (Functional Pearl) William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might (University of Utah, USA) Artifacts Reusable Article: icfp17main-main35-p (type: Full Paper) doi:
	Canou, Benjamin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Scaling up Functional Programming ..." Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC Benjamin Canou, Roberto Di Cosmo, and Grégoire Henry (OCamlPro, France; Inria, France; University of Paris Diderot, France) Article: icfp17main-main52-p (type: Full Paper) doi:
	Castagna, Giuseppe	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Typing with Union ..." Gradual Typing with Union and Intersection Types Giuseppe Castagna and Victor Lanvin (CNRS, France; University of Paris Diderot, France; ENS Cachan, France) Article: icfp17main-main22-p (type: Full Paper) doi:
	Chang, Stephen	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Super 8 Languages for Making ..." Super 8 Languages for Making Movies (Functional Pearl) Leif Andersen, Stephen Chang, and Matthias Felleisen (Northeastern University, USA) Artifacts Reusable Article: icfp17main-main93-p (type: Full Paper) doi:
	Cheney, James	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Imperative Functional Programs ..." Imperative Functional Programs That Explain Their Work Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney (University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main64-p (type: Full Paper) doi:
	Chlipala, Adam	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Kami: A Platform for High-Level ..." Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind (Massachusetts Institute of Technology, USA) Artifacts Functional Article: icfp17main-main16-p (type: Full Paper) doi:
	Choi, Joonwon	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Kami: A Platform for High-Level ..." Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind (Massachusetts Institute of Technology, USA) Artifacts Functional Article: icfp17main-main16-p (type: Full Paper) doi:
	Chong, Stephen	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Whip: Higher-Order Contracts ..." Whip: Higher-Order Contracts for Modern Services Lucas Waye, Stephen Chong, and Christos Dimoulas (Harvard University, USA) Artifacts Reusable Article: icfp17main-main58-p (type: Full Paper) doi:
	Cosman, Benjamin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Local Refinement Typing ..." Local Refinement Typing Benjamin Cosman and Ranjit Jhala (University of California at San Diego, USA) Artifacts Reusable Article: icfp17main-main8-p (type: Full Paper) doi:
	Dal Lago, Ugo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Automating Sized-Type Inference ..." Automating Sized-Type Inference for Complexity Analysis Martin Avanzini and Ugo Dal Lago (University of Innsbruck, Austria; University of Bologna, Italy; Inria, France) Article: icfp17main-main32-p (type: Full Paper) doi:
	Darais, David	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Abstracting Definitional Interpreters ..." Abstracting Definitional Interpreters (Functional Pearl) David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn (University of Maryland, USA) Artifacts Reusable Article: icfp17main-main114-p (type: Full Paper) doi:
	Davis, Milo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "No-Brainer CPS Conversion ..." No-Brainer CPS Conversion (Functional Pearl) Milo Davis, William Meehan, and Olin Shivers (Northeastern University, USA) Article: icfp17main-main104-p (type: Full Paper) doi:
	De Amorim, Pedro Henrique Azevedo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Specification for Dependent ..." A Specification for Dependent Types in Haskell Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg (University of Pennsylvania, USA; École Polytechnique, France; University of Campinas, Brazil; Bryn Mawr College, USA) Artifacts Reusable Article: icfp17main-main82-p (type: Full Paper) doi:
	Delignat-Lavaud, Antoine	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	De Moura, Leonardo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Metaprogramming Framework ..." A Metaprogramming Framework for Formal Verification Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura (Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA) Artifacts Reusable Article: icfp17main-main19-p (type: Full Paper) doi:
	Devriese, Dominique	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Parametric Quantifiers for ..." Parametric Quantifiers for Dependent Type Theory Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese (KU Leuven, Belgium; Chalmers University of Technology, Sweden) Artifacts Reusable Article: icfp17main-main41-p (type: Full Paper) doi:
	Di Cosmo, Roberto	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Scaling up Functional Programming ..." Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC Benjamin Canou, Roberto Di Cosmo, and Grégoire Henry (OCamlPro, France; Inria, France; University of Paris Diderot, France) Article: icfp17main-main52-p (type: Full Paper) doi:
	Dimoulas, Christos	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Whip: Higher-Order Contracts ..." Whip: Higher-Order Contracts for Modern Services Lucas Waye, Stephen Chong, and Christos Dimoulas (Harvard University, USA) Artifacts Reusable Article: icfp17main-main58-p (type: Full Paper) doi:
	Ebner, Gabriel	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Metaprogramming Framework ..." A Metaprogramming Framework for Formal Verification Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura (Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA) Artifacts Reusable Article: icfp17main-main19-p (type: Full Paper) doi:
	Eisenberg, Richard A.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Specification for Dependent ..." A Specification for Dependent Types in Haskell Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg (University of Pennsylvania, USA; École Polytechnique, France; University of Campinas, Brazil; Bryn Mawr College, USA) Artifacts Reusable Article: icfp17main-main82-p (type: Full Paper) doi: Proc. ACM Program. Lang., vol. 1, issue ICFP: "Constrained Type Families ..." Constrained Type Families J. Garrett Morris and Richard A. Eisenberg (University of Edinburgh, UK; Bryn Mawr College, USA) Artifacts Functional Article: icfp17main-main89-p (type: Full Paper) doi:
	Elliott, Conal	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Compiling to Categories ..." Compiling to Categories Conal Elliott (Target, USA) Article: icfp17main-main36-p (type: Full Paper) doi: Proc. ACM Program. Lang., vol. 1, issue ICFP: "Generic Functional Parallel ..." Generic Functional Parallel Algorithms: Scan and FFT Conal Elliott (Target, USA) Article: icfp17main-main48-p (type: Full Paper) doi:
	Ernst, Michael D.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Felleisen, Matthias	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Super 8 Languages for Making ..." Super 8 Languages for Making Movies (Functional Pearl) Leif Andersen, Stephen Chang, and Matthias Felleisen (Northeastern University, USA) Artifacts Reusable Article: icfp17main-main93-p (type: Full Paper) doi:
	Feltey, Daniel	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Herbarium Racketensis: A Stroll ..." Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler (Northwestern University, USA) Artifacts Reusable Article: icfp17main-main105-p (type: Full Paper) doi:
	Findler, Robert Bruce	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Herbarium Racketensis: A Stroll ..." Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler (Northwestern University, USA) Artifacts Reusable Article: icfp17main-main105-p (type: Full Paper) doi:
	Florence, Spencer P.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Herbarium Racketensis: A Stroll ..." Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler (Northwestern University, USA) Artifacts Reusable Article: icfp17main-main105-p (type: Full Paper) doi:
	Forster, Yannick	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On the Expressive Power of ..." On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar (Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia) Artifacts Functional Article: icfp17main-main39-p (type: Full Paper) doi:
	Fournet, Cédric	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Gaboardi, Marco	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Relational Logic for Higher-Order ..." A Relational Logic for Higher-Order Programs Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub (IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France) Artifacts Functional Article: icfp17main-main81-p (type: Full Paper) doi:
	Garg, Deepak	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Relational Logic for Higher-Order ..." A Relational Logic for Higher-Order Programs Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub (IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France) Artifacts Functional Article: icfp17main-main81-p (type: Full Paper) doi:
	Haeberlen, Andreas	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Framework for Adaptive Differential ..." A Framework for Adaptive Differential Privacy Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce (University of Pennsylvania, USA) Artifacts Functional Article: icfp17main-main109-p (type: Full Paper) doi:
	Hamana, Makoto	Proc. ACM Program. Lang., vol. 1, issue ICFP: "How to Prove Your Calculus ..." How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation Makoto Hamana (Gunma University, Japan) Article: icfp17main-main57-p (type: Full Paper) doi:
	Henry, Grégoire	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Scaling up Functional Programming ..." Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC Benjamin Canou, Roberto Di Cosmo, and Grégoire Henry (OCamlPro, France; Inria, France; University of Paris Diderot, France) Article: icfp17main-main52-p (type: Full Paper) doi:
	Heule, Stefan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Hirzel, Martin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Prototyping a Query Compiler ..." Prototyping a Query Compiler using Coq (Experience Report) Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon (IBM Research, USA) Artifacts Functional Article: icfp17main-main75-p (type: Full Paper (12 pages of text + references)) doi:
	Hriţcu, Cătălin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Igarashi, Atsushi	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Session Types ..." Gradual Session Types Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler (Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK) Artifacts Reusable Article: icfp17main-main76-p (type: Full Paper) doi: Proc. ACM Program. Lang., vol. 1, issue ICFP: "On Polymorphic Gradual Typing ..." On Polymorphic Gradual Typing Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi (Kyoto University, Japan; IBM Research, Japan) Artifacts Functional Article: icfp17main-main50-p (type: Full Paper) doi:
	Igarashi, Yuu	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On Polymorphic Gradual Typing ..." On Polymorphic Gradual Typing Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi (Kyoto University, Japan; IBM Research, Japan) Artifacts Functional Article: icfp17main-main50-p (type: Full Paper) doi:
	Jamner, Dustin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Theorems for Free for Free: ..." Theorems for Free for Free: Parametricity, With and Without Types Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler (Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main102-p (type: Full Paper) doi:
	Jhala, Ranjit	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Local Refinement Typing ..." Local Refinement Typing Benjamin Cosman and Ranjit Jhala (University of California at San Diego, USA) Artifacts Reusable Article: icfp17main-main8-p (type: Full Paper) doi:
	Justesen, Mathias Nygaard	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Effect-Driven QuickChecking ..." Effect-Driven QuickChecking of Compilers Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson (DTU, Denmark) Artifacts Functional Article: icfp17main-main67-p (type: Full Paper) doi:
	Kammar, Ohad	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On the Expressive Power of ..." On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar (Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia) Artifacts Functional Article: icfp17main-main39-p (type: Full Paper) doi:
	Kasting, Patrick	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Effect-Driven QuickChecking ..." Effect-Driven QuickChecking of Compilers Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson (DTU, Denmark) Artifacts Functional Article: icfp17main-main67-p (type: Full Paper) doi:
	Kesner, Delia	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Foundations of Strong Call ..." Foundations of Strong Call by Need Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner (LRI, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina; Stevens Institute of Technology, USA) Article: icfp17main-main65-p (type: Full Paper) doi:
	Krishnamurthi, Shriram	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Inferring Scope through Syntactic ..." Inferring Scope through Syntactic Sugar Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand (Brown University, USA; Northeastern University, USA) Artifacts Reusable Article: icfp17main-main45-p (type: Full Paper) doi:
	Kumar, Ramana	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verifying Efficient Function ..." Verifying Efficient Function Calls in CakeML Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan (University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA) Artifacts Reusable Article: icfp17main-main86-p (type: Full Paper) doi:
	Labich, Nicholas	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Abstracting Definitional Interpreters ..." Abstracting Definitional Interpreters (Functional Pearl) David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn (University of Maryland, USA) Artifacts Reusable Article: icfp17main-main114-p (type: Full Paper) doi:
	Lanvin, Victor	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Typing with Union ..." Gradual Typing with Union and Intersection Types Giuseppe Castagna and Victor Lanvin (CNRS, France; University of Paris Diderot, France; ENS Cachan, France) Article: icfp17main-main22-p (type: Full Paper) doi:
	Lindley, Sam	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On the Expressive Power of ..." On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar (Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia) Artifacts Functional Article: icfp17main-main39-p (type: Full Paper) doi:
	Lyubomirsky, Steven	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Mainland, Geoffrey	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Better Living through Operational ..." Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols Geoffrey Mainland (Drexel University, USA) Artifacts Reusable Article: icfp17main-main107-p (type: Full Paper) doi:
	Mandel, Louis	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Prototyping a Query Compiler ..." Prototyping a Query Compiler using Coq (Experience Report) Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon (IBM Research, USA) Artifacts Functional Article: icfp17main-main75-p (type: Full Paper (12 pages of text + references)) doi:
	Meehan, William	Proc. ACM Program. Lang., vol. 1, issue ICFP: "No-Brainer CPS Conversion ..." No-Brainer CPS Conversion (Functional Pearl) Milo Davis, William Meehan, and Olin Shivers (Northeastern University, USA) Article: icfp17main-main104-p (type: Full Paper) doi:
	Melgratti, Hernán	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Chaperone Contracts for Higher-Order ..." Chaperone Contracts for Higher-Order Sessions Hernán Melgratti and Luca Padovani (University of Buenos Aires, Argentina; University of Turin, Italy) Artifacts Reusable Article: icfp17main-main54-p (type: Full Paper) doi:
	Midtgaard, Jan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Effect-Driven QuickChecking ..." Effect-Driven QuickChecking of Compilers Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson (DTU, Denmark) Artifacts Functional Article: icfp17main-main67-p (type: Full Paper) doi:
	Might, Matthew	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Unified Approach to Solving ..." A Unified Approach to Solving Seven Programming Problems (Functional Pearl) William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might (University of Utah, USA) Artifacts Reusable Article: icfp17main-main35-p (type: Full Paper) doi:
	Morris, J. Garrett	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Constrained Type Families ..." Constrained Type Families J. Garrett Morris and Richard A. Eisenberg (University of Edinburgh, UK; Bryn Mawr College, USA) Artifacts Functional Article: icfp17main-main89-p (type: Full Paper) doi:
	Myreen, Magnus O.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verifying Efficient Function ..." Verifying Efficient Function Calls in CakeML Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan (University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA) Artifacts Reusable Article: icfp17main-main86-p (type: Full Paper) doi:
	Narayanan, Praveen	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Symbolic Conditioning of Arrays ..." Symbolic Conditioning of Arrays in Probabilistic Programs Praveen Narayanan and Chung-chieh Shan (Indiana University, USA) Artifacts Reusable Article: icfp17main-main100-p (type: Full Paper) doi:
	Nguyen, Phúc C.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Abstracting Definitional Interpreters ..." Abstracting Definitional Interpreters (Functional Pearl) David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn (University of Maryland, USA) Artifacts Reusable Article: icfp17main-main114-p (type: Full Paper) doi:
	Nielson, Flemming	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Effect-Driven QuickChecking ..." Effect-Driven QuickChecking of Compilers Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson (DTU, Denmark) Artifacts Functional Article: icfp17main-main67-p (type: Full Paper) doi:
	Nielson, Hanne Riis	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Effect-Driven QuickChecking ..." Effect-Driven QuickChecking of Compilers Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson (DTU, Denmark) Artifacts Functional Article: icfp17main-main67-p (type: Full Paper) doi:
	Nilsson, Henrik	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Testing and Debugging Functional ..." Testing and Debugging Functional Reactive Programming Ivan Perez and Henrik Nilsson (University of Nottingham, UK) Article: icfp17main-main70-p (type: Full Paper) doi:
	Norrish, Michael	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verifying Efficient Function ..." Verifying Efficient Function Calls in CakeML Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan (University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA) Artifacts Reusable Article: icfp17main-main86-p (type: Full Paper) doi:
	Nuyts, Andreas	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Parametric Quantifiers for ..." Parametric Quantifiers for Dependent Type Theory Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese (KU Leuven, Belgium; Chalmers University of Technology, Sweden) Artifacts Reusable Article: icfp17main-main41-p (type: Full Paper) doi:
	Owens, Scott	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verifying Efficient Function ..." Verifying Efficient Function Calls in CakeML Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan (University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA) Artifacts Reusable Article: icfp17main-main86-p (type: Full Paper) doi:
	Padovani, Luca	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Chaperone Contracts for Higher-Order ..." Chaperone Contracts for Higher-Order Sessions Hernán Melgratti and Luca Padovani (University of Buenos Aires, Argentina; University of Turin, Italy) Artifacts Reusable Article: icfp17main-main54-p (type: Full Paper) doi:
	Perera, Roly	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Imperative Functional Programs ..." Imperative Functional Programs That Explain Their Work Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney (University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main64-p (type: Full Paper) doi:
	Perez, Ivan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Testing and Debugging Functional ..." Testing and Debugging Functional Reactive Programming Ivan Perez and Henrik Nilsson (University of Nottingham, UK) Article: icfp17main-main70-p (type: Full Paper) doi:
	Pfenning, Frank	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Manifest Sharing with Session ..." Manifest Sharing with Session Types Stephanie Balzer and Frank Pfenning (Carnegie Mellon University, USA) Article: icfp17main-main85-p (type: Full Paper) doi:
	Pierce, Benjamin C.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Framework for Adaptive Differential ..." A Framework for Adaptive Differential Privacy Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce (University of Pennsylvania, USA) Artifacts Functional Article: icfp17main-main109-p (type: Full Paper) doi:
	Pombrio, Justin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Inferring Scope through Syntactic ..." Inferring Scope through Syntactic Sugar Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand (Brown University, USA; Northeastern University, USA) Artifacts Reusable Article: icfp17main-main45-p (type: Full Paper) doi:
	Pottier, François	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Visitors Unchained ..." Visitors Unchained François Pottier (Inria, France) Article: icfp17main-main55-p (type: Full Paper) doi:
	Pretnar, Matija	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On the Expressive Power of ..." On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar (Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia) Artifacts Functional Article: icfp17main-main39-p (type: Full Paper) doi:
	Protzenko, Jonathan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Puente, Juan Pedro Bolívar	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Persistence for the Masses: ..." Persistence for the Masses: RRB-Vectors in a Systems Language Juan Pedro Bolívar Puente Artifacts Functional Article: icfp17main-main68-p (type: Full Paper) doi:
	Ramananandro, Tahina	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Rastogi, Aseem	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Ricciotti, Wilmer	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Imperative Functional Programs ..." Imperative Functional Programs That Explain Their Work Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney (University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main64-p (type: Full Paper) doi:
	Roesch, Jared	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Metaprogramming Framework ..." A Metaprogramming Framework for Formal Verification Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura (Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA) Artifacts Reusable Article: icfp17main-main19-p (type: Full Paper) doi:
	Rosenblatt, Gregory	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Unified Approach to Solving ..." A Unified Approach to Solving Seven Programming Problems (Functional Pearl) William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might (University of Utah, USA) Artifacts Reusable Article: icfp17main-main35-p (type: Full Paper) doi:
	Roth, Aaron	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Framework for Adaptive Differential ..." A Framework for Adaptive Differential Privacy Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce (University of Pennsylvania, USA) Artifacts Functional Article: icfp17main-main109-p (type: Full Paper) doi:
	Sekiyama, Taro	Proc. ACM Program. Lang., vol. 1, issue ICFP: "On Polymorphic Gradual Typing ..." On Polymorphic Gradual Typing Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi (Kyoto University, Japan; IBM Research, Japan) Artifacts Functional Article: icfp17main-main50-p (type: Full Paper) doi:
	Shan, Chung-chieh	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Symbolic Conditioning of Arrays ..." Symbolic Conditioning of Arrays in Probabilistic Programs Praveen Narayanan and Chung-chieh Shan (Indiana University, USA) Artifacts Reusable Article: icfp17main-main100-p (type: Full Paper) doi:
	Sherman, Benjamin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Kami: A Platform for High-Level ..." Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind (Massachusetts Institute of Technology, USA) Artifacts Functional Article: icfp17main-main16-p (type: Full Paper) doi:
	Shinnar, Avraham	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Prototyping a Query Compiler ..." Prototyping a Query Compiler using Coq (Experience Report) Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon (IBM Research, USA) Artifacts Functional Article: icfp17main-main75-p (type: Full Paper (12 pages of text + references)) doi:
	Shivers, Olin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "No-Brainer CPS Conversion ..." No-Brainer CPS Conversion (Functional Pearl) Milo Davis, William Meehan, and Olin Shivers (Northeastern University, USA) Article: icfp17main-main104-p (type: Full Paper) doi:
	Siek, Jeremy G.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Theorems for Free for Free: ..." Theorems for Free for Free: Parametricity, With and Without Types Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler (Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main102-p (type: Full Paper) doi:
	Siméon, Jérôme	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Prototyping a Query Compiler ..." Prototyping a Query Compiler using Coq (Experience Report) Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jérôme Siméon (IBM Research, USA) Artifacts Functional Article: icfp17main-main75-p (type: Full Paper (12 pages of text + references)) doi:
	Smith, Chris	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Lock-Step Simulation Is Child's ..." Lock-Step Simulation Is Child's Play (Experience Report) Joachim Breitner and Chris Smith (University of Pennsylvania, USA; Google, USA) Artifacts Functional Article: icfp17main-main24-p (type: Full Paper) doi:
	Spivey, Michael	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Faster Coroutine Pipelines ..." Faster Coroutine Pipelines Michael Spivey (University of Oxford, UK) Artifacts Reusable Article: icfp17main-main14-p (type: Full Paper) doi:
	St-Amour, Vincent	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Herbarium Racketensis: A Stroll ..." Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler (Northwestern University, USA) Artifacts Reusable Article: icfp17main-main105-p (type: Full Paper) doi:
	Stolarek, Jan	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Imperative Functional Programs ..." Imperative Functional Programs That Explain Their Work Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney (University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main64-p (type: Full Paper) doi:
	Strub, Pierre-Yves	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Relational Logic for Higher-Order ..." A Relational Logic for Higher-Order Programs Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub (IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, France) Artifacts Functional Article: icfp17main-main81-p (type: Full Paper) doi:
	Swamy, Nikhil	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Tan, Yong Kiam	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verifying Efficient Function ..." Verifying Efficient Function Calls in CakeML Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan (University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA) Artifacts Reusable Article: icfp17main-main86-p (type: Full Paper) doi:
	Tatlock, Zachary	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Thiemann, Peter	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Session Types ..." Gradual Session Types Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler (Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK) Artifacts Reusable Article: icfp17main-main76-p (type: Full Paper) doi:
	Torlak, Emina	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Ullrich, Sebastian	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Metaprogramming Framework ..." A Metaprogramming Framework for Formal Verification Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura (Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA) Artifacts Reusable Article: icfp17main-main19-p (type: Full Paper) doi:
	Van Horn, David	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Abstracting Definitional Interpreters ..." Abstracting Definitional Interpreters (Functional Pearl) David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn (University of Maryland, USA) Artifacts Reusable Article: icfp17main-main114-p (type: Full Paper) doi:
	Vasconcelos, Vasco T.	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Session Types ..." Gradual Session Types Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler (Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK) Artifacts Reusable Article: icfp17main-main76-p (type: Full Paper) doi:
	Vezzosi, Andrea	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Parametric Quantifiers for ..." Parametric Quantifiers for Dependent Type Theory Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese (KU Leuven, Belgium; Chalmers University of Technology, Sweden) Artifacts Reusable Article: icfp17main-main41-p (type: Full Paper) doi: Proc. ACM Program. Lang., vol. 1, issue ICFP: "Normalization by Evaluation ..." Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France) Artifacts Reusable Article: icfp17main-main84-p (type: Full Paper) doi:
	Vijayaraghavan, Muralidaran	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Kami: A Platform for High-Level ..." Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind (Massachusetts Institute of Technology, USA) Artifacts Functional Article: icfp17main-main16-p (type: Full Paper) doi:
	Voizard, Antoine	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Specification for Dependent ..." A Specification for Dependent Types in Haskell Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg (University of Pennsylvania, USA; École Polytechnique, France; University of Campinas, Brazil; Bryn Mawr College, USA) Artifacts Reusable Article: icfp17main-main82-p (type: Full Paper) doi:
	Wadler, Philip	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Gradual Session Types ..." Gradual Session Types Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler (Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK) Artifacts Reusable Article: icfp17main-main76-p (type: Full Paper) doi: Proc. ACM Program. Lang., vol. 1, issue ICFP: "Theorems for Free for Free: ..." Theorems for Free for Free: Parametricity, With and Without Types Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler (Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK) Artifacts Functional Article: icfp17main-main102-p (type: Full Paper) doi:
	Wand, Mitchell	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Inferring Scope through Syntactic ..." Inferring Scope through Syntactic Sugar Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand (Brown University, USA; Northeastern University, USA) Artifacts Reusable Article: icfp17main-main45-p (type: Full Paper) doi:
	Wang, Peng	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Waye, Lucas	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Whip: Higher-Order Contracts ..." Whip: Higher-Order Contracts for Modern Services Lucas Waye, Stephen Chong, and Christos Dimoulas (Harvard University, USA) Artifacts Reusable Article: icfp17main-main58-p (type: Full Paper) doi:
	Weirich, Stephanie	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Specification for Dependent ..." A Specification for Dependent Types in Haskell Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg (University of Pennsylvania, USA; École Polytechnique, France; University of Campinas, Brazil; Bryn Mawr College, USA) Artifacts Reusable Article: icfp17main-main82-p (type: Full Paper) doi:
	Weitz, Konstantin	Proc. ACM Program. Lang., vol. 1, issue ICFP: "SpaceSearch: A Library for ..." SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock (University of Washington, USA; Stanford University, USA) Artifacts Reusable Article: icfp17main-main71-p (type: Full Paper) doi:
	Winograd-Cort, Daniel	Proc. ACM Program. Lang., vol. 1, issue ICFP: "A Framework for Adaptive Differential ..." A Framework for Adaptive Differential Privacy Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce (University of Pennsylvania, USA) Artifacts Functional Article: icfp17main-main109-p (type: Full Paper) doi:
	Winterhalter, Theo	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Normalization by Evaluation ..." Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France) Artifacts Reusable Article: icfp17main-main84-p (type: Full Paper) doi:
	Yallop, Jeremy	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Staged Generic Programming ..." Staged Generic Programming Jeremy Yallop (University of Cambridge, UK) Article: icfp17main-main121-p (type: Full Paper) doi:
	You, Shu-Hung	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Herbarium Racketensis: A Stroll ..." Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler (Northwestern University, USA) Artifacts Reusable Article: icfp17main-main105-p (type: Full Paper) doi:
	Zanella-Béguelin, Santiago	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:
	Zinzindohoué, Jean-Karim	Proc. ACM Program. Lang., vol. 1, issue ICFP: "Verified Low-Level Programming ..." Verified Low-Level Programming Embedded in F* Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy (Microsoft Research, USA; Inria, France; Massachusetts Institute of Technology, USA) Artifacts Reusable Article: icfp17main-main96-p (type: Full Paper) doi:

139 authors

proc time: 0.11