Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 3 SepDisplayed time zone: Belfast change
Sun 3 Sep
Displayed time zone: Belfast change
09:00 - 09:10 | |||
09:00 10mTalk | Welcome PLMW Brigitte Pientka McGill University, Neel Krishnaswami Computer Laboratory, University of Cambridge, Daniel R. Licata Wesleyan University |
09:00 - 09:05 | |||
09:00 5mDay opening | Welcome TyDe |
09:00 - 09:10 | |||
09:00 10mDay opening | Welcome HOPE |
09:00 - 10:00 | |||
09:00 60mTalk | Tutorial T1: Writing Verified Programs in CakeML Tutorials P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden |
09:05 - 10:00 | |||
09:05 55mTalk | Driving types into PHP TyDe Andrew Kennedy Facebook London |
09:10 - 10:00 | |||
09:10 50mTalk | Keynote PLMW Chris Martens North Carolina State University |
09:10 - 10:00 | |||
09:10 60mTalk | Invited Talk: Semantics of Effect Systems by Graded Monads HOPE Shin-ya Katsumata National Institute of Informatics |
09:10 - 10:10 | |||
09:10 60mTalk | Keynote Scheme Sam Tobin-Hochstadt Indiana University |
10:00 - 10:30 | |||
10:00 30mCoffee break | Sunday coffee break 1 Catering |
10:30 - 11:30 | |||
10:30 30mTalk | A Few Frank Remarks PLMW | ||
11:00 30mTalk | Compositional Compiler Correctness PLMW Amal Ahmed Northeastern University, USA File Attached |
10:30 - 11:30 | |||
10:30 30mTalk | Generic packet descriptions: verified parsing and pretty printing of low-level data TyDe | ||
11:00 30mTalk | Structured asynchrony with algebraic effects TyDe Daan Leijen Microsoft Research |
10:30 - 11:30 | |||
10:30 30mTalk | Higher-order Programming is an Effect HOPE File Attached | ||
11:00 30mTalk | A monadic solution to the Cartwright-Felleisen-Wadler conjecture HOPE File Attached |
10:30 - 11:30 | |||
10:30 45mTalk | Paper: Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation Scheme Satoshi Egi Rakuten Institute of Technology | ||
11:15 15mTalk | Lightning Talk: Extending the LISP model from cons cells to triples, from trees to hypergraphs Scheme |
10:30 - 11:30 | |||
10:30 60mTalk | Tutorial T1: Writing Verified Programs in CakeML (part 2) Tutorials P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden |
11:20 - 12:00 | |||
11:20 40mCoffee break | Sunday coffee break 2 Catering |
12:00 - 12:30 | |||
12:00 30mTalk | Not How To Do Your PhD PLMW Gabriel Scherer Northeastern University File Attached |
12:00 - 12:25 | |||
12:00 25mTalk | Cogent⇑: giving systems engineers a stepping stone TyDe Zilin Chen UNSW, Australia |
12:00 - 12:30 | |||
12:00 30mTalk | RustBelt: Securing the Foundations of the Rust Programming Language HOPE Ralf Jung MPI-SWS, Germany, Jacques-Henri Jourdan MPI-SWS, Germany, Robbert Krebbers Delft University of Technology, Netherlands, Derek Dreyer MPI-SWS |
12:00 - 12:30 | |||
12:00 30mTalk | Panel: Future of Scheme Scheme François-René Rideau , Marc Feeley Université de Montréal, Arthur Gleckler SRFI Editor, Kathy Gray , Alaric Snell-Pym , Andy Wingo Igalia, S.L. |
12:00 - 12:30 | |||
12:00 30mTalk | Tutorial T1: Writing Verified Programs in CakeML (part 3) Tutorials P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden |
12:25 - 14:00 | |||
12:25 1h35mLunch | Sunday lunch Catering |
14:00 - 15:00 | |||
14:00 30mTalk | Gradual Typing PLMW Ronald Garcia University of British Columbia File Attached | ||
14:30 30mTalk | Scala: Types in Theory & Practice PLMW Nada Amin University of Cambridge File Attached |
14:00 - 15:00 | |||
14:00 30mTalk | Type safe Redis queries -- a case study of type-level programming in Haskell TyDe Ting-Yan Lai Institute of Information Science, Academia Sinica, Tyng-Ruey Chuang Institute of Information Science, Academia Sinica, Shin-Cheng Mu Academia Sinica, Taiwan | ||
14:30 30mTalk | Type-directed diffing of structured data TyDe Victor Cacciari Miraldo University of Utrecht, Pierre-Evariste Dagand LIP6/CNRS , Wouter Swierstra University of Utrecht |
14:00 - 15:00 | |||
14:00 30mTalk | Handling fibred algebraic effects HOPE Danel Ahman University of Edinburgh | ||
14:30 30mTalk | Only Control Effects and Dependent Types HOPE |
14:00 - 15:00 | |||
14:00 45mTalk | Paper: Toward Parallelizing Control-flow Analysis with Datalog Scheme | ||
14:45 15mTalk | Lightning: Gerbil on Gambit, as they say Racket on Chez Scheme |
14:00 - 15:00 | |||
14:00 60mTalk | Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL Tutorials P: Jasmin Blanchette Vrije Universiteit Amsterdam, P: Andreas Lochbihler , P: Andrei Popescu Middlesex University, London, P: Dmitriy Traytel ETH Zurich |
14:50 - 15:30 | |||
14:50 40mCoffee break | Sunday coffee break 3 Catering |
15:30 - 16:30 | |||
15:30 60mTalk | How to Write Papers and Give Talks That People Can Follow PLMW Derek Dreyer MPI-SWS Media Attached |
15:30 - 16:20 | |||
15:30 25mTalk | Affine killing TyDe | ||
15:55 25mTalk | On ringads and foldables TyDe James McKinna University of Edinburgh |
15:30 - 16:30 | |||
15:30 30mTalk | Programming a Web Server with Algebraic Effects HOPE Daan Leijen Microsoft Research | ||
16:00 30mTalk | Logical Relations for Algebraic Effects HOPE Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk , Filip Sieczkowski University of Wrocław |
15:30 - 16:30 | |||
15:30 45mTalk | Report: Status of the ongoing R7RS standardization process Scheme | ||
16:15 15mTalk | Lightning: {lambda talk} Scheme |
15:30 - 16:20 | |||
15:30 50mTalk | Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 2) Tutorials Jasmin Blanchette Vrije Universiteit Amsterdam, Andreas Lochbihler , Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich |
16:20 - 16:50 | |||
16:20 30mCoffee break | Sunday coffee break 4 Catering |
16:50 - 17:40 | |||
16:50 50mTalk | Panel Discussion: Careers in Programming Languages PLMW Sam Staton University of Oxford, Richard A. Eisenberg Bryn Mawr College, USA, Andreas Rossberg Google, Daan Leijen , Amal Ahmed Northeastern University, USA |
16:50 - 17:40 | |||
16:50 25mTalk | Type oriented programming for task based parallelism TyDe | ||
17:15 25mTalk | Type-directed reasoning for probabilistic, non-compositional resources TyDe Edwin Brady University of St. Andrews, UK, Kevin Hammond University of St. Andrews, UK, Christopher Schwaab University of St Andrews |
16:50 - 17:40 | |||
16:50 30mTalk | Recalling a Witness HOPE Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, n.n., Cédric Fournet Microsoft Research, n.n. Pre-print |
16:50 - 17:50 | |||
16:50 50mTalk | Invited Talk Scheme Matthew Might University of Utah, USA | ||
17:40 10mDay closing | Goodbye Scheme |
16:50 - 17:50 | |||
16:50 60mTalk | Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 3) Tutorials P: Jasmin Blanchette Vrije Universiteit Amsterdam, P: Andreas Lochbihler , P: Andrei Popescu Middlesex University, London, P: Dmitriy Traytel ETH Zurich |
Mon 4 SepDisplayed time zone: Belfast change
Mon 4 Sep
Displayed time zone: Belfast change
09:00 - 10:00 | Monday KeynoteKeynotes and Reports at L1 Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
09:00 60mTalk | Compositional creativity: some principles for talking to computersKeynote Keynotes and Reports |
10:00 - 10:30 | |||
10:00 30mCoffee break | Monday coffee break 1 Catering |
10:30 - 12:00 | |||
10:30 22mTalk | Super 8 Languages for Making Movies (Functional Pearl) Research Papers Leif Andersen Northeastern University, USA, Stephen Chang Northeastern University, USA, Matthias Felleisen Northeastern University, USA DOI | ||
10:52 22mTalk | Testing and Debugging Functional Reactive Programming Research Papers DOI | ||
11:15 22mTalk | Lock-Step Simulation Is Child's Play (Experience Report) Research Papers DOI | ||
11:37 22mTalk | Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC Research Papers Benjamin Canou OCamlPro, n.n., Roberto Di Cosmo Inria, France / University of Paris Diderot, France, Grégoire Henry OCamlPro, n.n. DOI |
10:30 - 10:45 | |||
10:30 15mOther | Welcome message FSCD |
10:45 - 11:45 | |||
10:45 60mTalk | Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages FSCD |
12:00 - 13:00 | |||
12:00 60mLunch | Monday lunch Catering |
13:00 - 14:30 | Functional Programming TechniquesResearch Papers at L1 Chair(s): Graham Hutton University of Nottingham | ||
13:00 22mTalk | Faster Coroutine Pipelines Research Papers Mike Spivey University of Oxford, UK DOI | ||
13:22 22mTalk | A Pretty But Not Greedy Printer (Functional Pearl) Research Papers Jean-Philippe Bernardy University of Gothenburg DOI | ||
13:45 22mTalk | Generic Functional Parallel Algorithms: Scan and FFT Research Papers Conal Elliott Target, USA DOI | ||
14:07 22mTalk | A Unified Approach to Solving Seven Programming Problems (Functional Pearl) Research Papers William E. Byrd University of Utah, USA, Michael Ballantyne University of Utah, USA, Gregory Rosenblatt n.n., n.n., Matthew Might University of Utah, USA DOI |
13:00 - 14:30 | |||
13:00 30mTalk | Polynomial running times for polynomial-time oracle machines FSCD | ||
13:30 30mTalk | A Curry-Howard Approach to Church’s Synthesis FSCD | ||
14:00 30mTalk | Streett Automata Model Checking of Higher-Order Recursion Schemes FSCD A: Ryota Suzuki , A: Koichi Fujima , A: Naoki Kobayashi University of Tokyo, Japan, A: Takeshi Tsukada University of Tokyo, Japan |
14:30 - 15:00 | |||
14:30 30mCoffee break | Monday coffee break 2 Catering |
15:00 - 16:10 | |||
15:00 23mTalk | Prototyping a Query Compiler using Coq (Experience Report) Research Papers Joshua Auerbach IBM Research, Martin Hirzel IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research, Jerome Simeon IBM Research DOI | ||
15:23 23mTalk | A Framework for Adaptive Differential Privacy Research Papers Daniel Winograd-Cort University of Pennsylvania, USA, Andreas Haeberlen University of Pennsylvania, USA, Aaron Roth University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania DOI | ||
15:46 23mTalk | Symbolic Conditioning of Arrays in Probabilistic Programs Research Papers DOI |
15:00 - 16:00 | |||
15:00 30mTalk | Relating System F and λ2: A Case Study in Coq, Abella and Beluga FSCD | ||
15:30 30mTalk | Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL FSCD Jasmin Blanchette Vrije Universiteit Amsterdam, A: Mathias Fleury MPI-INF, A: Dmitriy Traytel ETH Zurich |
16:10 - 16:40 | |||
16:10 30mCoffee break | Monday coffee break 3 Catering |
16:40 - 18:10 | |||
16:40 22mTalk | Abstracting Definitional Interpreters Research Papers David Darais University of Maryland, USA, Nicholas Labich University of Maryland, USA, Phúc C. Nguyễn University of Maryland, USA, David Van Horn University of Maryland, USA DOI | ||
17:02 22mTalk | On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Research Papers Yannick Forster Saarland University, Germany / University of Cambridge, UK, Ohad Kammar University of Oxford, UK, Sam Lindley University of Edinburgh, UK, Matija Pretnar University of Ljubljana, Slovenia DOI | ||
17:25 22mTalk | Imperative Functional Programs That Explain Their Work Research Papers Wilmer Ricciotti University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, Roly Perera University of Edinburgh, UK / University of Glasgow, UK, James Cheney University of Edinburgh, UK DOI | ||
17:47 22mTalk | Effect-Driven QuickChecking of Compilers Research Papers Jan Midtgaard DTU, Denmark, Mathias Nygaard Justesen DTU, Denmark, Patrick Kasting DTU, Denmark, Flemming Nielson DTU, Denmark, Hanne Riis Nielson DTU, Denmark DOI |
16:40 - 18:10 | |||
16:40 30mTalk | A polynomial-time algorithm for the Lambek calculus with brackets of bounded order FSCD | ||
17:10 30mTalk | A sequent calculus for semi-associativity FSCD | ||
17:40 30mTalk | Combinatorial Flows and their Normalisation FSCD |
18:10 - 18:20 | Monday Closing EventsKeynotes and Reports at L1 Chair(s): Peter Thiemann University of Freiburg, Germany | ||
18:10 10mDay closing | Monday Announcements Keynotes and Reports |
18:30 - 20:30 | |||
18:30 2hSocial Event | Welcome Reception Social Events |
Tue 5 SepDisplayed time zone: Belfast change
Tue 5 Sep
Displayed time zone: Belfast change
09:00 - 10:00 | |||
09:00 60mTalk | Assuring AIKeynote Keynotes and Reports |
10:00 - 10:30 | |||
10:00 30mCoffee break | Tuesday coffee break 1 Catering |
10:30 - 12:00 | Low-level and Systems ProgrammingResearch Papers at L1 Chair(s): Sam Tobin-Hochstadt Indiana University | ||
10:30 22mTalk | Persistence for the Masses: RRB-Vectors in a Systems Language Research Papers Juan Pedro Bolívar Puente Independent Consultant, Sinusoidal Engineering DOI Pre-print | ||
10:52 22mTalk | Verified Low-Level Programming Embedded in F* Research Papers Jonathan Protzenko Microsoft Research, n.n., Jean-Karim Zinzindohoué Inria, France, Aseem Rastogi Microsoft Research, Tahina Ramananandro Microsoft Research, n.n., Peng Wang Massachusetts Institute of Technology, USA, Santiago Zanella-Béguelin Microsoft Research, n.n., Antoine Delignat-Lavaud Microsoft Research, n.n., Cătălin Hriţcu Inria Paris, Karthikeyan Bhargavan Inria, France, Cédric Fournet Microsoft Research, n.n., Nikhil Swamy Microsoft Research, n.n. DOI | ||
11:15 22mTalk | Verifying Efficient Function Calls in CakeML Research Papers Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan Carnegie Mellon University, USA DOI | ||
11:37 22mTalk | Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols Research Papers Geoffrey Mainland Drexel University, USA DOI |
10:30 - 11:30 | |||
10:30 60mTalk | Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses FSCD Georg Moser University of Innsbruck |
11:30 - 12:00 | |||
11:30 30mTalk | Continuation Passing Style for Effect Handlers FSCD A: Daniel Hillerström The University of Edinburgh, A: Sam Lindley University of Edinburgh, UK, A: Robert Atkey University of Strathclyde, A: KC Sivaramakrishnan University of Cambridge |
12:00 - 13:00 | |||
12:00 60mLunch | Tuesday lunch Catering |
13:00 - 14:30 | Foundations of Higher-Order ProgrammingResearch Papers at L1 Chair(s): Gabriel Scherer Northeastern University | ||
13:00 22mTalk | How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation Research Papers Makoto Hamana Gunma University, Japan DOI | ||
13:22 22mTalk | A Relational Logic for Higher-Order Programs Research Papers Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Spain, Marco Gaboardi University at Buffalo, SUNY, USA, Deepak Garg MPI-SWS, Germany, Pierre-Yves Strub École Polytechnique, n.n. DOI | ||
13:45 22mTalk | Foundations of Strong Call by Need Research Papers Thibaut Balabonski LRI, France / University of Paris-Sud, France, Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia Kesner Université de Paris, CNRS, IRIF, France DOI | ||
14:07 22mTalk | No-Brainer CPS Conversion Research Papers Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA DOI |
14:30 - 15:00 | |||
14:30 30mCoffee break | Tuesday coffee break 2 Catering |
15:00 - 16:10 | |||
15:00 23mTalk | Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Research Papers Joonwon Choi Massachusetts Institute of Technology, USA, Muralidaran Vijayaraghavan Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology, USA, A: Arvind Massachusetts Institute of Technology, USA DOI | ||
15:23 23mTalk | SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Research Papers Konstantin Weitz University of Washington, USA, Steven Lyubomirsky University of Washington, USA, Stefan Heule Stanford University, USA, Emina Torlak University of Washington, USA, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle DOI | ||
15:46 23mTalk | Local Refinement Typing Research Papers Benjamin Cosman University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA DOI |
15:00 - 16:00 | |||
15:00 30mTalk | Is the optimal implementation inefficient? Elementarily not FSCD | ||
15:30 30mTalk | Optimality and the Linear Substitution Calculus FSCD A: Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, A: Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina |
16:10 - 16:40 | |||
16:10 30mCoffee break | Tuesday coffee break 3 Catering |
16:40 - 17:50 | |||
16:40 23mTalk | Compiling to Categories Research Papers Conal Elliott Target, USA DOI | ||
17:03 23mTalk | Visitors Unchained Research Papers François Pottier Inria, France DOI | ||
17:26 23mTalk | Staged Generic Programming Research Papers Jeremy Yallop University of Cambridge, UK DOI Pre-print |
16:40 - 18:10 | |||
16:40 30mTalk | Generalized Refocusing: from Hybrid Strategies to Abstract Machines FSCD | ||
17:10 30mTalk | Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or FSCD | ||
17:40 30mTalk | Refutation of Sallé's Longstanding Conjecture FSCD |
17:50 - 18:20 | |||
17:50 30mTalk | Programming Contest Report Keynotes and Reports |
Wed 6 SepDisplayed time zone: Belfast change
Wed 6 Sep
Displayed time zone: Belfast change
09:00 - 09:37 | |||
09:00 37mAwards | Student Research Competition: Finalist Presentations Student Research Competition |
09:00 - 10:00 | |||
09:00 60mTalk | Quantitative semantics for probabilistic programming FSCD |
09:37 - 10:00 | |||
09:37 23mTalk | Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Research Papers Vincent St-Amour Northwestern University, USA, Daniel Feltey Northwestern University, USA, Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Robert Bruce Findler Northwestern University, USA DOI |
10:00 - 10:30 | |||
10:00 30mCoffee break | Wednesday coffee break 1 Catering |
10:30 - 12:00 | |||
10:30 22mTalk | A Specification for Dependent Types in Haskell Research Papers Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvania, USA, Pedro Henrique Azevedo de Amorim Ecole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. Eisenberg Bryn Mawr College, USA DOI | ||
10:52 22mTalk | Parametric Quantifiers for Dependent Type Theory Research Papers Andreas Nuyts KU Leuven, Belgium, Andrea Vezzosi Chalmers University of Technology, Sweden, Dominique Devriese KU Leuven, Belgium DOI | ||
11:15 22mTalk | Normalization by Evaluation for Sized Dependent Types Research Papers Andreas Abel University of Gothenburg, Sweden, Andrea Vezzosi Chalmers University of Technology, Sweden, Théo Winterhalter ENS Paris-Saclay, France DOI | ||
11:37 22mTalk | A Metaprogramming Framework for Formal Verification Research Papers Gabriel Ebner Vienna University of Technology, Austria, Sebastian Ullrich KIT, Germany, Jared Roesch University of Washington, USA, Jeremy Avigad Carnegie Mellon University, USA, Leonardo de Moura Microsoft Research, n.n. DOI |
10:30 - 12:00 | |||
10:30 30mTalk | Displayed categories FSCD | ||
11:00 30mTalk | List Objects with Algebraic Structure FSCD | ||
11:30 30mTalk | There is only one notion of differentiation FSCD |
12:00 - 13:00 | |||
12:00 60mLunch | Wednesday lunch Catering |
13:00 - 14:30 | |||
13:00 22mTalk | Chaperone Contracts for Higher-Order Sessions Research Papers DOI | ||
13:22 22mTalk | Whip: Higher-Order Contracts for Modern Services Research Papers Lucas Waye Harvard University, USA, Christos Dimoulas Harvard University, USA, Stephen Chong Harvard University, USA DOI | ||
13:45 22mTalk | Manifest Sharing with Session Types Research Papers DOI | ||
14:07 22mTalk | Gradual Session Types Research Papers Atsushi Igarashi Kyoto University, Japan, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, Portugal, Philip Wadler University of Edinburgh, UK DOI |
13:00 - 14:30 | |||
13:00 30mTalk | A Fibrational Framework for Substructural and Modal Logics FSCD | ||
13:30 30mTalk | Dinaturality between syntax and semantics FSCD | ||
14:00 30mTalk | Models of Type Theory Based on Moore Paths FSCD |
14:30 - 15:00 | |||
14:30 30mCoffee break | Wednesday coffee break 2 Catering |
15:00 - 16:10 | Integrating Static and Dynamic TypingResearch Papers at L1 Chair(s): Ronald Garcia University of British Columbia | ||
15:00 23mTalk | Theorems for Free for Free: Parametricity, With and Without Types Research Papers Amal Ahmed Northeastern University, USA, Dustin Jamner Northeastern University, USA, Jeremy G. Siek Indiana University, USA, Philip Wadler University of Edinburgh, UK DOI | ||
15:23 23mTalk | On Polymorphic Gradual Typing Research Papers Yuu Igarashi Kyoto University, Japan, Taro Sekiyama IBM Research, Japan, Atsushi Igarashi Kyoto University, Japan DOI | ||
15:46 23mTalk | Gradual Typing with Union and Intersection Types Research Papers Giuseppe Castagna CNRS, France / University of Paris Diderot, France, Victor Lanvin ENS Cachan, France DOI |
15:00 - 16:00 | |||
15:00 30mTalk | Böhm Reduction in Infinitary Term Graph Rewriting Systems FSCD | ||
15:30 30mTalk | Infinite Runs in Abstract Completion FSCD |
16:10 - 16:40 | |||
16:10 30mCoffee break | Wednesday coffee break 3 Catering |
16:40 - 17:50 | |||
16:40 23mTalk | Constrained Type Families Research Papers DOI | ||
17:03 23mTalk | Automating Sized-Type Inference for Complexity Analysis Research Papers Martin Avanzini University of Innsbruck, Austria, Ugo Dal Lago University of Bologna, Italy / Inria, France DOI | ||
17:26 23mTalk | Inferring Scope through Syntactic Sugar Research Papers Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA, Mitchell Wand Northeastern University, USA DOI |
16:40 - 17:10 | |||
16:40 30mTalk | Negative Translations and Normal Modality FSCD |
17:10 - 17:20 | |||
17:10 10mOther | Termination and Complexity Competition 2017 FSCD |
17:20 - 18:10 | |||
17:20 50mMeeting | FSCD General Meeting FSCD |
17:50 - 18:00 | |||
17:50 10mAwards | Student Research Competition Awards Student Research Competition |
18:00 - 18:20 | |||
18:00 10mTalk | Program Chair's Report Keynotes and Reports | ||
18:10 10mTalk | ICFP 2018 Announcement Keynotes and Reports |
18:30 - 22:30 | |||
18:30 4hSocial Event | Banquet Social Events |
Thu 7 SepDisplayed time zone: Belfast change
Thu 7 Sep
Displayed time zone: Belfast change
09:00 - 10:00 | |||
09:00 60mTalk | Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk) Haskell Didier Rémy INRIA |
09:00 - 10:00 | |||
09:00 60mTalk | Type systems for the relational verification of higher order programs FSCD |
09:00 - 09:05 | |||
09:00 5mDay opening | Welcome ML |
09:00 - 09:10 | |||
09:00 10mDay opening | Welcome to FHPC'17 FHPC |
09:00 - 10:00 | |||
09:00 60mOther | Tutorial C2: Extensible Effects: understanding them, implementing them, using them CUFP |
09:00 - 10:00 | |||
09:00 60mOther | Tutorial C1: Online Applications with Incremental CUFP |
09:05 - 10:00 | |||
09:05 55mTalk | State machines all the way down ML Edwin Brady University of St. Andrews, UK |
09:10 - 10:10 | |||
09:10 60mTalk | Haskell in the Datacentre FHPC Simon Marlow Facebook |
10:00 - 10:30 | |||
10:00 30mCoffee break | Thursday coffee break 1 Catering |
10:30 - 11:30 | |||
10:30 30mTalk | Algebraic Graphs with Class (Functional Pearl) Haskell | ||
11:00 30mTalk | Packrats Parse in Packs Haskell |
10:30 - 11:59 | |||
10:30 30mTalk | Arrays and References in Resource Aware ML FSCD | ||
11:00 30mTalk | The Complexity of Principal Inhabitation FSCD | ||
11:30 29mTalk | Types as Resources for Classical Natural Deduction FSCD |
10:30 - 11:45 | |||
10:30 25mTalk | Mergeable types ML Gowtham Kaki Purdue University, KC Sivaramakrishnan University of Cambridge, Samodya Abeysiriwardane Purdue University, Suresh Jagannathan Purdue University | ||
10:55 25mTalk | Tierless modules ML Gabriel Radanne Université Denis Diderot Paris 7, PPS, Jérôme Vouillon Univ Paris Diderot, Sorbonne Paris Cité, BeSport | ||
11:20 25mTalk | First-class subtypes ML |
10:30 - 11:30 | |||
10:30 30mTalk | From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation FHPC | ||
11:00 30mTalk | Destination-Passing Style for Efficient Memory Management FHPC A: Amir Shaikhha EPFL, Switzerland, A: Andrew Fitzgibbon Microsoft Research, Cambridge, A: Simon Peyton Jones Microsoft Research, Cambridge, A: Dimitrios Vytiniotis Microsoft Research, Cambridge |
10:30 - 11:30 | |||
10:30 60mTalk | Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 2) CUFP |
10:30 - 11:30 | |||
10:30 60mTalk | Tutorial C1: Online Applications with Incremental (part 2) CUFP |
11:20 - 12:00 | |||
11:20 40mCoffee break | Thursday coffee break 2 Catering |
12:00 - 12:30 | |||
12:00 30mTalk | Ode on a Random Urn (Functional Pearl) Haskell |
12:00 - 12:25 | |||
12:00 25mTalk | VOCAL -- a verified OCAml Library ML Arthur Charguéraud Inria, Jean-Christophe Filliatre CNRS, Paris, France, Mário Pereira LRI - Université Paris-Sud, François Pottier Inria, France |
12:00 - 12:30 | |||
12:00 30mTalk | VisPar: Visualising dataflow graphs from the Par monad FHPC A: Maximilian Algehed Chalmers University of Technology, Sweden, A: Patrik Jansson Chalmers University of Technology |
12:00 - 12:30 | |||
12:00 30mTalk | Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 3) CUFP |
12:00 - 12:30 | |||
12:00 30mTalk | Tutorial C1: Online Applications with Incremental (part 3) CUFP |
12:25 - 14:00 | |||
12:25 1h35mLunch | Thursday lunch Catering |
14:00 - 15:00 | |||
14:00 30mDemonstration | QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration) Haskell Maximilian Algehed Chalmers University of Technology, Sweden, Koen Claessen Chalmers University of Technology, Moa Johansson Chalmers University of Technology, Nicholas Smallbone | ||
14:30 30mTalk | Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results Haskell |
14:00 - 15:15 | |||
14:00 25mTalk | Typer: an infix statically typed Lisp ML Pierre Delaunay Université de Montréal, Vincent Archambault-Bouffard Université de Montréal, Stefan Monnier Université de Montréal | ||
14:25 25mTalk | Relational conversion for OCaml ML | ||
14:50 25mTalk | Towards abductive functional programming ML Koko Muroya University of Birmingham, UK |
14:00 - 15:00 | |||
14:00 30mTalk | In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions FHPC | ||
14:30 30mTalk | Strategies for Regular Segmented Reductions on GPU FHPC A: Rasmus Wriedt Larsen DIKU, University of Copenhagen, A: Troels Henriksen DIKU, University of Copenhagen |
14:00 - 15:00 | |||
14:00 60mOther | Tutorial C3: Concurrent Programming with Effect Handlers CUFP |
14:00 - 15:00 | |||
14:00 60mTalk | Tutorial C4: Git under the hood with OCaml CUFP |
14:50 - 15:30 | |||
14:50 40mCoffee break | Thursday coffee break 3 Catering |
15:30 - 16:30 | |||
15:30 30mTalk | Using Coq to Write Fast and Correct Haskell Haskell | ||
16:00 30mTalk | A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq Haskell |
15:30 - 16:20 | |||
15:30 25mTalk | Making SML# a general-purpose high-performance language ML Atsushi Ohori Tohoku University, Japan, Kenjiro Taura The University of Tokyo, Katsuhiro Ueno Tohoku University | ||
15:55 25mTalk | Efficient representation of large, dynamic sequences in ML ML |
15:30 - 16:30 | |||
15:30 29mDemonstration | Futhark Demo FHPC Troels Henriksen DIKU, University of Copenhagen | ||
16:00 29mDemonstration | ParaFormance Demo: Democratizing Parallel Software Development FHPC | ||
16:30 20mSocial Event | Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine FHPC |
15:30 - 16:20 | |||
15:30 50mTalk | Tutorial C3: Concurrent Programming with Effect Handlers (part 2) CUFP |
15:30 - 16:20 | |||
15:30 50mTalk | Tutorial C4: Git under the hood with OCaml (part 2) CUFP |
16:20 - 16:50 | |||
16:20 30mCoffee break | Thursday coffee break 4 Catering |
16:50 - 17:50 | |||
16:50 30mTalk | A Meta-EDSL for Distributed Web Applications Haskell Anton Ekblad Chalmers University of Technology | ||
17:20 30mTalk | Composable Network Stacks and Remote Monads Haskell |
16:50 - 17:40 | |||
16:50 25mTalk | Effects without monads: non-determinism ML | ||
17:15 25mTalk | Effectively tackling the awkward squad ML Stephen Dolan , Spiros Eliopoulos Jane Street Group, Daniel Hillerström The University of Edinburgh, Anil Madhavapeddy OCaml Labs, KC Sivaramakrishnan University of Cambridge, Leo White Jane Street |
16:50 - 17:50 | |||
16:50 30mDemonstration | Ziria Demo: Wringing performance from high-level code FHPC | ||
17:20 30mDay closing | Panel Discussion: The challenges for Functional High Performance Computing FHPC Geoffrey Mainland Drexel University, USA, Kevin Hammond University of St. Andrews, UK, Simon Marlow Facebook |
16:50 - 17:30 | |||
16:50 40mTalk | Tutorial C3: Concurrent Programming with Effect Handlers (part 3) CUFP |
16:50 - 17:30 | |||
16:50 40mTalk | Tutorial C4: Git under the hood with OCaml (part 3) CUFP |
18:15 - 20:30 | |||
18:15 2h15mSocial Event | Industry Reception Social Events |
Fri 8 SepDisplayed time zone: Belfast change
Fri 8 Sep
Displayed time zone: Belfast change
09:00 - 10:00 | |||
09:00 60mTalk | Algorithmic Music in Haskell (Invited Talk) Haskell Donya Quick Stevens Institute of Technology |
09:00 - 09:10 | |||
09:00 5mDay opening | Opening OCaml Gabriel Scherer Northeastern University |
09:00 - 09:10 | |||
09:00 10mDay opening | Opening & Welcome Erlang |
09:00 - 10:00 | |||
09:00 60mTalk | Tutorial C6: Transducers in Practice CUFP Renzo Borgatti uSwitch |
09:00 - 10:00 | |||
09:00 60mTalk | Tutorial C5: Teaching Functional Programming CUFP Michael Sperber Active Group GmbH |
09:10 - 10:10 | |||
09:05 35mTalk | Invited talk: new contributors OCaml | ||
09:40 25mTalk | The State of the OCaml Platform: September 2017 OCaml Anil Madhavapeddy OCaml Labs |
09:10 - 10:00 | |||
09:10 50mTalk | Keynote Erlang |
10:00 - 10:30 | |||
10:00 30mCoffee break | Friday coffee break 1 Catering |
10:30 - 11:30 | |||
10:30 30mTalk | Well-Typed Music Does Not Sound Wrong (Experience Report) Haskell | ||
11:00 30mTalk | Back to the Future: Time Travel in FRP Haskell Ivan Perez University of Nottingham, UK |
10:30 - 11:30 | |||
10:30 20mTalk | Owl: A General-Purpose Numerical Library in OCaml OCaml Liang Wang University of Cambridge Link to publication Pre-print | ||
10:50 20mTalk | Extending OCaml's open OCaml Link to publication Pre-print | ||
11:10 20mTalk | Genspio: Generating Shell Phrases In OCaml OCaml Sebastien Mondet Mount Sinai - Hammer Lab Pre-print |
10:30 - 11:20 | |||
10:30 25mTalk | Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm Erlang Evgeniy Shishkin JSC "InfoTeCS" DOI File Attached | ||
10:55 25mTalk | Towards an Isabelle/HOL Formalisation of Core Erlang Erlang Joseph Harrison University of Kent |
10:30 - 11:30 | |||
10:30 60mTalk | Tutorial C6: Transducers in Practice (part 2) CUFP |
10:30 - 11:30 | |||
10:30 60mTalk | Tutorial C5: Teaching Functional Programming (part 2) CUFP |
11:20 - 12:00 | |||
11:20 40mCoffee break | Friday coffee break 2 Catering |
11:35 - 12:30 | |||
11:35 10mTalk | Flash poster presentation OCaml | ||
11:45 45mTalk | mSAT: An OCaml SAT Solver OCaml Bury Guillaume INRIA / LSV / CNRS Link to publication | ||
11:45 45mTalk | Jbuilder: a modern approach to OCaml development OCaml | ||
11:45 45mTalk | Tyre – Typed Regular Expressions OCaml Gabriel Radanne Université Denis Diderot Paris 7, PPS Link to publication | ||
11:45 45mTalk | ocamli: Interpreted OCaml OCaml Link to publication |
12:00 - 12:30 | |||
12:00 30mTalk | The Linearity Monad Haskell |
12:00 - 12:25 | |||
12:00 25mTalk | Erlang and Elixir development news Erlang |
12:00 - 12:30 | |||
12:00 30mTalk | Tutorial C6: Transducers in Practice (part 3) CUFP |
12:00 - 12:30 | |||
12:00 30mTalk | Tutorial C5: Teaching Functional Programming (part 3) CUFP |
12:25 - 14:00 | |||
12:25 1h35mLunch | Friday lunch Catering |
14:00 - 15:00 | |||
14:00 30mTalk | Elaboration on Functional Dependencies Haskell | ||
14:30 30mTalk | Quantified Class Constraints Haskell Gert-Jan Bottu , Georgios Karachalias KU Leuven, Belgium, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, China, Philip Wadler University of Edinburgh, UK |
14:00 - 15:00 | |||
14:00 20mTalk | ROTOR: First Steps Towards a Refactoring Tool for OCaml OCaml Link to publication | ||
14:20 20mTalk | A memory model for multicore OCaml OCaml Link to publication | ||
14:40 20mTalk | Bioinformatics, The Typed Tagless Final Way OCaml Sebastien Mondet Mount Sinai - Hammer Lab Pre-print |
14:00 - 14:50 | |||
14:00 25mTalk | Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang Erlang Kagumi Azuma Kwansei Gakuin University, Nagisa Ishiura Kwansei Gakuin University, Nobuaki Yoshida ASTEM RI/KYOTO, Hiroyuki Kanbara ASTEM RI/KYOTO | ||
14:25 25mTalk | Structuring Erlang BEAM control flow Erlang |
14:00 - 15:00 | |||
14:00 60mTalk | Tutorial C8: GraphQL Servers in OCaml CUFP |
14:00 - 15:00 | |||
14:00 60mTalk | Tutorial C7: Owl - Data Science in OCaml CUFP |
14:50 - 15:30 | |||
14:50 40mCoffee break | Friday coffee break 3 Catering |
15:30 - 16:30 | |||
15:30 30mTalk | Hardware Software Co-Design in Haskell Haskell | ||
16:00 30mTalk | Streaming Irregular Arrays Haskell Robert Clifton-Everest , Trevor L. McDonell University of New South Wales, Australia, Manuel Chakravarty , Gabriele Keller Data61,CSIRO (formerly NICTA) and UNSW |
15:30 - 16:30 | |||
15:30 20mTalk | A B-tree library for OCaml OCaml Tom Ridge University of Leicester, UK Link to publication | ||
15:50 20mTalk | Wodan: a pure OCaml, flash-aware filesystem library OCaml Gabriel de Perthuis OCaml Labs Link to publication | ||
16:10 20mTalk | Tezos: the OCaml Crypto-Ledger OCaml Benjamin Canou OCamlPro, n.n., Grégoire Henry OCamlPro, n.n., Pierre Chambart OCamlPRO, Fabrice Le Fessant OCamlPro, Arthur BREITMAN Dynamic Ledger Solutions |
15:30 - 16:20 | |||
15:30 25mTalk | The Shared-Memory Interferences of Erlang/OTP Built-ins Erlang | ||
15:55 25mTalk | Towards Change-driven Testing Erlang |
15:30 - 16:20 | |||
15:30 50mTalk | Tutorial C8: GraphQL Servers in OCaml (part 2) CUFP |
15:30 - 16:20 | |||
15:30 50mTalk | Tutorial C7: Owl - Data Science in OCaml (part 2) CUFP |
16:20 - 16:50 | |||
16:20 30mCoffee break | Friday coffee break 4 Catering |
16:50 - 17:50 | |||
16:50 30mTalk | Improving STM Performance with Transactional Structs Haskell | ||
17:20 30mTalk | Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping Haskell |
16:50 - 17:40 | |||
17:00 20mTalk | Component-based Program Synthesis in OCaml OCaml Link to publication | ||
17:20 20mTalk | Testing with Crowbar OCaml |
16:50 - 17:50 | |||
16:50 30mTalk | eAOP - An Aspect Oriented Programming Framework for Erlang Erlang Ian Cassar University of Malta, Adrian Francalanza University of Malta, Luca Aceto Reykjavik University, Anna Ingolfsdottir Reykjavik University | ||
17:20 30mTalk | In medias res: WIP discussion Erlang |
16:50 - 17:30 | |||
16:50 40mTalk | Tutorial C8: GraphQL Servers in OCaml (part 3) CUFP |
16:50 - 17:30 | |||
16:50 40mTalk | Tutorial C7: Owl - Data Science in OCaml (part 3) CUFP |
Sat 9 SepDisplayed time zone: Belfast change
Sat 9 Sep
Displayed time zone: Belfast change
09:00 - 10:10 | |||
09:00 30mTalk | Progress on GHC HIW Simon Peyton Jones Microsoft Research, Cambridge | ||
09:30 30mTalk | GHC Infrastructure Update and Discussion HIW Ben Gamari Well-Typed LLP | ||
10:00 10mTalk | Getting Ready for Hadrian HIW |
09:00 - 09:10 | |||
09:00 10mDay opening | Welcome FARM |
09:10 - 10:00 | |||
09:10 25mTalk | Keynote: Are We There Yet? CUFP Bodil Stokke Church of Emacs | ||
09:35 25mTalk | Bonsai: a DSL for serverless firm real-time decisioning CUFP Jeremie Lasalle-Ratelle AppNexus |
09:10 - 10:00 | |||
09:10 30mTalk | A Categorial Grammar for Music and Its Use in Automatic Melody Generation FARM | ||
09:40 20mDemonstration | Demo — Representation of Musical Notation in Haskell FARM Pre-print |
10:00 - 10:30 | |||
10:00 30mCoffee break | Saturday coffee break 1 Catering |
10:30 - 11:30 | |||
10:30 25mTalk | Native Support for Explicit Stacks in LLVM HIW | ||
10:55 25mTalk | SimplexHC: Lowering High-Level Haskell to Imperative IR HIW Siddharth Bhat IIT Hyderabad | ||
11:20 10mTalk | Lightning Talk Slot #1 HIW |
10:30 - 11:20 | |||
10:30 25mTalk | Interfacing OCaml and Rust: picking the right tool for the job CUFP Joris Giovannangeli Ahrefs Research | ||
10:55 25mTalk | Distributed load testing with MZBench CUFP |
10:30 - 11:30 | |||
10:30 20mDemonstration | Demo — African Polyphony and Polyrhythm FARM Chris Ford ThoughtWorks (UK) Ltd. Pre-print | ||
10:50 20mDemonstration | Demo — Vivid: Sound Synthesis with Haskell and SuperCollider FARM Pre-print | ||
11:10 30mTalk | GALE: A Functional Graphic Adventure Library and Engine FARM Ivan Perez University of Nottingham, UK |
11:20 - 12:00 | |||
11:20 40mCoffee break | Saturday coffee break 2 Catering |
12:00 - 12:25 | |||
12:00 25mTalk | On Unsatisfiability HIW J. Garrett Morris University of Kansas, USA |
12:00 - 12:25 | |||
12:00 25mTalk | Gens N' Roses: Appetite for Reduction CUFP Jacob Stanley Ambiata |
12:00 - 12:30 | |||
12:00 30mTalk | Modelling the Way Mathematics Is Actually Done FARM |
12:25 - 14:00 | |||
12:25 1h35mLunch | Saturday lunch Catering |
14:00 - 15:00 | |||
14:00 25mTalk | Why GHC Core and Linear Logic Should be Best Friends HIW | ||
14:25 25mTalk | Demand Analysis vs. Call Arity HIW Sebastian Graf Karlsruhe Institute of Technology | ||
14:50 10mTalk | Lightning Talk Slot #2 HIW |
14:00 - 14:50 | |||
14:00 25mTalk | Formally Verifying a Smart-Contract Language Implementation with Isabelle CUFP Simon Meier Digital Asset | ||
14:25 25mTalk | Haskell games and apps for iOS and Android CUFP Ivan Perez University of Nottingham, UK |
14:00 - 15:00 | |||
14:00 60mTalk | FAUST Tutorial for Functional Programmers FARM |
14:50 - 15:30 | |||
14:50 40mCoffee break | Saturday coffee break 3 Catering |
15:30 - 16:30 | |||
15:30 25mTalk | IDE Support in GHC HIW | ||
15:55 25mTalk | Tracking GHC Performance HIW | ||
16:20 10mTalk | Lightning Talk Slot #3 HIW |
15:30 - 16:20 | |||
15:30 25mTalk | Using Haskell to run a datacenter CUFP | ||
15:55 25mTalk | Functional Facades over Legacy Code CUFP |
15:30 - 16:20 | |||
15:30 20mDemonstration | Demo — The Arpeggigon: A Functional Reactive Musical Automaton FARM Henrik Nilsson University of Nottingham, UK Pre-print | ||
15:50 20mDemonstration | Demo — Ait: A Concatenative Language for Creative Programming FARM Pre-print |
16:20 - 16:50 | |||
16:20 30mCoffee break | Saturday coffee break 4 Catering |
16:50 - 17:50 | |||
16:50 25mTalk | An Experiment in Fragment-Based Code Distribution HIW Philipp Schuster University of Tübingen | ||
17:15 35mTalk | Lightning Talk Slot #4 HIW |
16:50 - 17:40 | |||
16:50 25mTalk | Building the largest payment sandbox on a tiny machine CUFP | ||
17:15 25mTalk | Using Functional Programming to Accelerate Translational Research at Pfizer CUFP Austin Huang Pfizer |
16:50 - 17:40 | |||
16:50 30mTalk | Unified Media Programming: An Algebraic Approach FARM Simon Archipoff CNRS LaBRI, Inria Bordeaux,, David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University | ||
17:20 20mDemonstration | Demo — Octopus: A High-Level Fast 3D Animation Language FARM Simon Archipoff CNRS LaBRI, Inria Bordeaux,, David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University Pre-print |
19:30 - 22:00 | |||
19:30 2h30mSocial Event | FARM Evening Of Algorithmic Arts Social Events |