Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom

Conference Dates
Conference Dates are in time zone (GMT+01:00) Belfast, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
Sun 3 Sep

Displayed time zone: Belfast change

09:00 - 09:10
WelcomePLMW at L1
Chair(s): Brigitte PientkaMcGill University
09:00
10m
Talk
Welcome
PLMW
Brigitte PientkaMcGill University, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Dan LicataWesleyan University
09:00 - 09:05
WelcomeTyDe at L2
09:00
5m
Day opening
Welcome
TyDe
Sam LindleyUniversity of Edinburgh, UK, Brent YorgeyHendrix College
09:00 - 09:10
WelcomeHOPE at L3
09:00
10m
Day opening
Welcome
HOPE
C: François PottierInria, France, C: Aleksandar NanevskiIMDEA Software Institute
09:00 - 09:10
Session 0Scheme at L4
09:00
10m
Day opening
Welcome
Scheme

09:00 - 10:00
Morning tutorial session 1Tutorials at L5
09:00
60m
Talk
Tutorial T1: Writing Verified Programs in CakeML
Tutorials
P: Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, P: Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, P: Scott OwensUniversity of Kent, UK, P: Magnus O. MyreenChalmers University of Technology, Sweden
09:05 - 10:00
Invited talkTyDe at L2
09:05
55m
Talk
Driving types into PHP
TyDe
Andrew KennedyFacebook London
09:10 - 10:00
KeynotePLMW at L1
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
09:10
50m
Talk
Keynote
PLMW
Chris MartensNorth Carolina State University
09:10 - 10:00
Invited talkHOPE at L3
09:10
60m
Talk
Invited Talk: Semantics of Effect Systems by Graded Monads
HOPE
Shin-ya KatsumataNational Institute of Informatics
09:10 - 10:10
Session 1Scheme at L4
09:10
60m
Talk
Keynote
Scheme
Sam Tobin-HochstadtIndiana University
10:00 - 10:30
Sunday coffee break 1Catering at Catering
10:00
30m
Coffee break
Sunday coffee break 1
Catering

10:30 - 11:30
Session 1PLMW at L1
10:30
30m
Talk
A Few Frank Remarks
PLMW
11:00
30m
Talk
Compositional Compiler Correctness
PLMW
Amal AhmedNortheastern University, USA
File Attached
10:30 - 11:30
Full papers 1TyDe at L2
10:30
30m
Talk
Generic packet descriptions: verified parsing and pretty printing of low-level data
TyDe
Marcell van GeestUtrecht University, Wouter SwierstraUniversity of Utrecht
11:00
30m
Talk
Structured asynchrony with algebraic effects
TyDe
Daan LeijenMicrosoft Research
10:30 - 11:30
Morning tutorial session 2Tutorials at L5
10:30
60m
Talk
Tutorial T1: Writing Verified Programs in CakeML (part 2)
Tutorials
P: Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, P: Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, P: Scott OwensUniversity of Kent, UK, P: Magnus O. MyreenChalmers University of Technology, Sweden
11:20 - 12:00
Sunday coffee break 2Catering at Catering
11:20
40m
Coffee break
Sunday coffee break 2
Catering

12:00 - 12:30
Session 2PLMW at L1
12:00
30m
Talk
Not How To Do Your PhD
PLMW
Gabriel SchererNortheastern University
File Attached
12:00 - 12:25
Extended abstracts 1TyDe at L2
12:00
25m
Talk
Cogent⇑: giving systems engineers a stepping stone
TyDe
Zilin ChenUNSW, Australia
12:00 - 12:30
RustHOPE at L3
12:00
30m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
HOPE
Ralf JungMPI-SWS, Germany, Jacques-Henri JourdanMPI-SWS, Germany, Robbert KrebbersDelft University of Technology, Netherlands, Derek DreyerMPI-SWS
12:00 - 12:30
Session 3Scheme at L4
12:00
30m
Talk
Panel: Future of Scheme
Scheme
François-René Rideau, Marc FeeleyUniversité de Montréal, Arthur GlecklerSRFI Editor, Kathy Gray, Alaric Snell-Pym, Andy WingoIgalia, S.L.
12:00 - 12:30
Morning tutorial session 3Tutorials at L5
12:00
30m
Talk
Tutorial T1: Writing Verified Programs in CakeML (part 3)
Tutorials
P: Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, P: Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, P: Scott OwensUniversity of Kent, UK, P: Magnus O. MyreenChalmers University of Technology, Sweden
12:25 - 14:00
Sunday lunchCatering at Catering
12:25
1h35m
Lunch
Sunday lunch
Catering

14:00 - 15:00
Session 3PLMW at L1
14:00
30m
Talk
Gradual Typing
PLMW
Ronald GarciaUniversity of British Columbia
File Attached
14:30
30m
Talk
Scala: Types in Theory & Practice
PLMW
Nada AminUniversity of Cambridge
File Attached
14:00 - 15:00
Full papers 2TyDe at L2
14:00
30m
Talk
Type safe Redis queries -- a case study of type-level programming in Haskell
TyDe
Ting-Yan LaiInstitute of Information Science, Academia Sinica, Tyng-Ruey ChuangInstitute of Information Science, Academia Sinica, Shin-Cheng MuAcademia Sinica, Taiwan
14:30
30m
Talk
Type-directed diffing of structured data
TyDe
Victor Cacciari MiraldoUniversity of Utrecht, Pierre-Evariste DagandLIP6/CNRS , Wouter SwierstraUniversity of Utrecht
14:00 - 15:00
Effects and Dependent TypesHOPE at L3
14:00
30m
Talk
Handling fibred algebraic effects
HOPE
Danel AhmanUniversity of Edinburgh
14:30
30m
Talk
Only Control Effects and Dependent Types
HOPE
Youyou CongOchanomizu University, William J. BowmanNortheastern University
14:00 - 15:00
Afternoon tutorial session 1Tutorials at L5
14:00
60m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL
Tutorials
P: Jasmin BlanchetteVrije Universiteit Amsterdam, P: Andreas Lochbihler, P: Andrei PopescuMiddlesex University, London, P: Dmitriy TraytelETH Zurich
14:50 - 15:30
Sunday coffee break 3Catering at Catering
14:50
40m
Coffee break
Sunday coffee break 3
Catering

15:30 - 16:20
Extended abstracts 2TyDe at L2
15:30
25m
Talk
Affine killing
TyDe
Kiko Fernandez-ReyesUppsala University, Dave ClarkeUppsala Univ. Sweden and KU Leuvern
15:55
25m
Talk
On ringads and foldables
TyDe
James McKinnaUniversity of Edinburgh
15:30 - 16:30
EffectsHOPE at L3
15:30
30m
Talk
Programming a Web Server with Algebraic Effects
HOPE
Daan LeijenMicrosoft Research
16:00
30m
Talk
Logical Relations for Algebraic Effects
HOPE
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr Polesiuk, Filip SieczkowskiUniversity of Wrocław
15:30 - 16:20
Afternoon tutorial session 2Tutorials at L5
15:30
50m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 2)
Tutorials
Jasmin BlanchetteVrije Universiteit Amsterdam, Andreas Lochbihler, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich
16:20 - 16:50
Sunday coffee break 4Catering at Catering
16:20
30m
Coffee break
Sunday coffee break 4
Catering

16:50 - 17:40
Session 5PLMW at L1
16:50
50m
Talk
Panel Discussion: Careers in Programming Languages
PLMW
Sam StatonUniversity of Oxford, Richard A. EisenbergBryn Mawr College, USA, Andreas RossbergGoogle, Daan Leijen, Amal AhmedNortheastern University, USA
16:50 - 17:40
Extended abstracts 3TyDe at L2
16:50
25m
Talk
Type oriented programming for task based parallelism
TyDe
17:15
25m
Talk
Type-directed reasoning for probabilistic, non-compositional resources
TyDe
Edwin BradyUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK, Christopher SchwaabUniversity of St Andrews
16:50 - 17:40
MonotonicityHOPE at L3
16:50
30m
Talk
Recalling a Witness
HOPE
Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, n.n., Cédric FournetMicrosoft Research, n.n.
Pre-print
16:50 - 17:50
Session 6Scheme at L4
16:50
50m
Talk
Invited Talk
Scheme
Matthew MightUniversity of Utah, USA
17:40
10m
Day closing
Goodbye
Scheme

16:50 - 17:50
Afternoon tutorial session 3Tutorials at L5
16:50
60m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 3)
Tutorials
P: Jasmin BlanchetteVrije Universiteit Amsterdam, P: Andreas Lochbihler, P: Andrei PopescuMiddlesex University, London, P: Dmitriy TraytelETH Zurich

Conference Day
Mon 4 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Monday KeynoteKeynotes and Reports at L1
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford
09:00
60m
Talk
Compositional creativity: some principles for talking to computersKeynote
Keynotes and Reports
K: Chris MartensNorth Carolina State University
10:00 - 10:30
Monday coffee break 1Catering at Catering
10:00
30m
Coffee break
Monday coffee break 1
Catering

10:30 - 12:00
Art and EducationResearch Papers at L1
Chair(s): Kathryn E. GrayUniversity of Cambridge
10:30
22m
Talk
Super 8 Languages for Making Movies (Functional Pearl)
Research Papers
Leif AndersenNortheastern University, USA, Stephen ChangNortheastern University, USA, Matthias FelleisenNortheastern University, USA
DOI
10:52
22m
Talk
Testing and Debugging Functional Reactive Programming
Research Papers
Ivan PerezUniversity of Nottingham, UK, Henrik NilssonUniversity of Nottingham, UK
DOI
11:15
22m
Talk
Lock-Step Simulation Is Child's Play (Experience Report)
Research Papers
Joachim BreitnerUniversity of Pennsylvania, Chris SmithGoogle, USA
DOI
11:37
22m
Talk
Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC
Research Papers
Benjamin CanouOCamlPro, n.n., Roberto Di CosmoInria, France / University of Paris Diderot, France, Grégoire HenryOCamlPro, n.n.
DOI
10:30 - 10:45
WelcomeFSCD at L2
10:30
15m
Other
Welcome message
FSCD
C: Sam StatonUniversity of Oxford, P: Dale MillerINRIA Saclay and LIX
10:45 - 11:45
Session 1FSCD at L2
10:45
60m
Talk
Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages
FSCD
I: Alexandra SilvaUniversity College London
12:00 - 13:00
Monday lunchCatering at Catering
12:00
60m
Lunch
Monday lunch
Catering

13:00 - 14:30
Functional Programming TechniquesResearch Papers at L1
Chair(s): Graham HuttonUniversity of Nottingham
13:00
22m
Talk
Faster Coroutine Pipelines
Research Papers
Mike SpiveyUniversity of Oxford, UK
DOI
13:22
22m
Talk
A Pretty But Not Greedy Printer (Functional Pearl)
Research Papers
Jean-Philippe BernardyUniversity of Gothenburg
DOI
13:45
22m
Talk
Generic Functional Parallel Algorithms: Scan and FFT
Research Papers
Conal ElliottTarget, USA
DOI
14:07
22m
Talk
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
Research Papers
William E. ByrdUniversity of Utah, USA, Michael BallantyneUniversity of Utah, USA, Gregory Rosenblattn.n., n.n., Matthew MightUniversity of Utah, USA
DOI
14:30 - 15:00
Monday coffee break 2Catering at Catering
14:30
30m
Coffee break
Monday coffee break 2
Catering

15:00 - 16:10
ApplicationsResearch Papers at L1
Chair(s): Alexandra SilvaUniversity College London
15:00
23m
Talk
Prototyping a Query Compiler using Coq (Experience Report)
Research Papers
Joshua AuerbachIBM Research, Martin HirzelIBM Research, Louis MandelIBM Research, Avraham ShinnarIBM Research, Jerome SimeonIBM Research
DOI
15:23
23m
Talk
A Framework for Adaptive Differential Privacy
Research Papers
Daniel Winograd-CortUniversity of Pennsylvania, USA, Andreas HaeberlenUniversity of Pennsylvania, USA, Aaron RothUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of Pennsylvania
DOI
15:46
23m
Talk
Symbolic Conditioning of Arrays in Probabilistic Programs
Research Papers
Praveen NarayananIndiana University, USA, Chung-chieh ShanIndiana University, USA
DOI
15:00 - 16:00
Session 3FSCD at L2
15:00
30m
Talk
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
FSCD
A: Jonas Kaiser, A: Brigitte PientkaMcGill University, A: Gert SmolkaSaarland University
15:30
30m
Talk
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
FSCD
Jasmin BlanchetteVrije Universiteit Amsterdam, A: Mathias FleuryMPI-INF, A: Dmitriy TraytelETH Zurich
16:10 - 16:40
Monday coffee break 3Catering at Catering
16:10
30m
Coffee break
Monday coffee break 3
Catering

16:40 - 18:10
EffectsResearch Papers at L1
Chair(s): Ben LippmeierDigital Asset / UNSW Australia
16:40
22m
Talk
Abstracting Definitional Interpreters
Research Papers
David DaraisUniversity of Maryland, USA, Nicholas LabichUniversity of Maryland, USA, Phúc C. NguyễnUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA
DOI
17:02
22m
Talk
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Research Papers
Yannick ForsterSaarland University, Germany / University of Cambridge, UK, Ohad KammarUniversity of Oxford, UK, Sam LindleyUniversity of Edinburgh, UK, Matija PretnarUniversity of Ljubljana, Slovenia
DOI
17:25
22m
Talk
Imperative Functional Programs That Explain Their Work
Research Papers
Wilmer RicciottiUniversity of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK, Roly PereraUniversity of Edinburgh, UK / University of Glasgow, UK, James CheneyUniversity of Edinburgh, UK
DOI
17:47
22m
Talk
Effect-Driven QuickChecking of Compilers
Research Papers
Jan MidtgaardDTU, Denmark, Mathias Nygaard JustesenDTU, Denmark, Patrick KastingDTU, Denmark, Flemming NielsonDTU, Denmark, Hanne Riis NielsonDTU, Denmark
DOI
18:10 - 18:20
Monday Closing EventsKeynotes and Reports at L1
Chair(s): Peter ThiemannUniversity of Freiburg, Germany
18:10
10m
Day closing
Monday Announcements
Keynotes and Reports

18:30 - 20:30
Welcome ReceptionSocial Events at Foyer
18:30
2h
Social Event
Welcome Reception
Social Events

Conference Day
Tue 5 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Tuesday KeynoteKeynotes and Reports at L1
Chair(s): Mark JonesPortland State University
09:00
60m
Talk
Assuring AIKeynote
Keynotes and Reports
I: John LaunchburyGalois, Inc.
10:00 - 10:30
Tuesday coffee break 1Catering at Catering
10:00
30m
Coffee break
Tuesday coffee break 1
Catering

10:30 - 12:00
Low-level and Systems ProgrammingResearch Papers at L1
Chair(s): Sam Tobin-HochstadtIndiana University
10:30
22m
Talk
Persistence for the Masses: RRB-Vectors in a Systems Language
Research Papers
Juan Pedro Bolívar PuenteIndependent Consultant, Sinusoidal Engineering
DOI Pre-print
10:52
22m
Talk
Verified Low-Level Programming Embedded in F*
Research Papers
Jonathan ProtzenkoMicrosoft Research, n.n., Jean-Karim ZinzindohouéInria, France, Aseem RastogiMicrosoft Research, Tahina RamananandroMicrosoft Research, n.n., Peng WangMassachusetts Institute of Technology, USA, Santiago Zanella-BéguelinMicrosoft Research, n.n., Antoine Delignat-LavaudMicrosoft Research, n.n., Cătălin HriţcuInria Paris, Karthikeyan BhargavanInria, France, Cédric FournetMicrosoft Research, n.n., Nikhil SwamyMicrosoft Research, n.n.
DOI
11:15
22m
Talk
Verifying Efficient Function Calls in CakeML
Research Papers
Scott OwensUniversity of Kent, UK, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanCarnegie Mellon University, USA
DOI
11:37
22m
Talk
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Research Papers
Geoffrey MainlandDrexel University, USA
DOI
10:30 - 11:30
Session 5FSCD at L2
10:30
60m
Talk
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses
FSCD
Georg MoserUniversity of Innsbruck
11:30 - 12:00
Session 6FSCD at L2
11:30
30m
Talk
Continuation Passing Style for Effect Handlers
FSCD
A: Daniel HillerströmThe University of Edinburgh, A: Sam LindleyUniversity of Edinburgh, UK, A: Robert AtkeyUniversity of Strathclyde, A: KC SivaramakrishnanUniversity of Cambridge
12:00 - 13:00
Tuesday lunchCatering at Catering
12:00
60m
Lunch
Tuesday lunch
Catering

13:00 - 14:30
Foundations of Higher-Order ProgrammingResearch Papers at L1
Chair(s): Gabriel SchererNortheastern University
13:00
22m
Talk
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Research Papers
Makoto HamanaGunma University, Japan
DOI
13:22
22m
Talk
A Relational Logic for Higher-Order Programs
Research Papers
Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Spain, Marco GaboardiUniversity at Buffalo, SUNY, USA, Deepak GargMPI-SWS, Germany, Pierre-Yves StrubÉcole Polytechnique, n.n.
DOI
13:45
22m
Talk
Foundations of Strong Call by Need
Research Papers
Thibaut BalabonskiLRI, France / University of Paris-Sud, France, Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia KesnerIRIF, France / University of Paris Diderot, France
DOI
14:07
22m
Talk
No-Brainer CPS Conversion
Research Papers
Milo DavisNortheastern University, USA, William MeehanNortheastern University, USA, Olin ShiversNortheastern University, USA
DOI
14:30 - 15:00
Tuesday coffee break 2Catering at Catering
14:30
30m
Coffee break
Tuesday coffee break 2
Catering

15:00 - 16:10
Tools for VerificationResearch Papers at L1
Chair(s): Nikhil SwamyMicrosoft Research, n.n.
15:00
23m
Talk
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Research Papers
Joonwon ChoiMassachusetts Institute of Technology, USA, Muralidaran VijayaraghavanMassachusetts Institute of Technology, USA, Benjamin ShermanMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology, USA, A: ArvindMassachusetts Institute of Technology, USA
DOI
15:23
23m
Talk
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Research Papers
Konstantin WeitzUniversity of Washington, USA, Steven LyubomirskyUniversity of Washington, USA, Stefan HeuleStanford University, USA, Emina TorlakUniversity of Washington, USA, Michael D. ErnstUniversity of Washington, USA, Zachary TatlockUniversity of Washington, Seattle
DOI
15:46
23m
Talk
Local Refinement Typing
Research Papers
Benjamin CosmanUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA
DOI
15:00 - 16:00
Session 8FSCD at L2
15:00
30m
Talk
Is the optimal implementation inefficient? Elementarily not
FSCD
A: Stefano Guerrini, A: Marco SolieriUniversity of Bath
15:30
30m
Talk
Optimality and the Linear Substitution Calculus
FSCD
A: Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, A: Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina
16:10 - 16:40
Tuesday coffee break 3Catering at Catering
16:10
30m
Coffee break
Tuesday coffee break 3
Catering

16:40 - 17:50
Program ConstructionResearch Papers at L1
Chair(s): John HughesChalmers University of Technology
16:40
23m
Talk
Compiling to Categories
Research Papers
Conal ElliottTarget, USA
DOI
17:03
23m
Talk
Visitors Unchained
Research Papers
François PottierInria, France
DOI
17:26
23m
Talk
Staged Generic Programming
Research Papers
Jeremy YallopUniversity of Cambridge, UK
DOI Pre-print
17:50 - 18:20
Tuesday Closing EventsKeynotes and Reports at L1
17:50
30m
Talk
Programming Contest Report
Keynotes and Reports
P: Sam LindleyUniversity of Edinburgh, UK

Conference Day
Wed 6 Sep

Displayed time zone: Belfast change

09:00 - 09:37
SRC PresentationsStudent Research Competition at L1
Chair(s): Ilya SergeyUniversity College London
09:00
37m
Awards
Student Research Competition: Finalist Presentations
Student Research Competition

09:37 - 10:00
Domain-Specific LanguagesResearch Papers at L1
Chair(s): Martin ErwigOregon State University
09:37
23m
Talk
Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
Research Papers
Vincent St-AmourNorthwestern University, USA, Daniel FelteyNorthwestern University, USA, Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Robby FindlerNorthwestern University, USA
DOI
10:00 - 10:30
Wednesday coffee break 1Catering at Catering
10:00
30m
Coffee break
Wednesday coffee break 1
Catering

10:30 - 12:00
Dependently Typed ProgrammingResearch Papers at L1
Chair(s): Dan LicataWesleyan University
10:30
22m
Talk
A Specification for Dependent Types in Haskell
Research Papers
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvania, USA, Pedro Henrique Azevedo de AmorimEcole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. EisenbergBryn Mawr College, USA
DOI
10:52
22m
Talk
Parametric Quantifiers for Dependent Type Theory
Research Papers
Andreas NuytsKU Leuven, Belgium, Andrea VezzosiChalmers University of Technology, Sweden, Dominique DevrieseKU Leuven, Belgium
DOI
11:15
22m
Talk
Normalization by Evaluation for Sized Dependent Types
Research Papers
Andreas AbelUniversity of Gothenburg, Sweden, Andrea VezzosiChalmers University of Technology, Sweden, Theo WinterhalterENS Paris-Saclay, France
DOI
11:37
22m
Talk
A Metaprogramming Framework for Formal Verification
Research Papers
Gabriel EbnerVienna University of Technology, Austria, Sebastian UllrichKIT, Germany, Jared RoeschUniversity of Washington, USA, Jeremy AvigadCarnegie Mellon University, USA, Leonardo de MouraMicrosoft Research, n.n.
DOI
10:30 - 12:00
Session 11FSCD at L2
10:30
30m
Talk
Displayed categories
FSCD
11:00
30m
Talk
List Objects with Algebraic Structure
FSCD
A: Marcelo FioreComputer Laboratory, University of Cambridge, A: Philip Saville
11:30
30m
Talk
There is only one notion of differentiation
FSCD
12:00 - 13:00
Wednesday lunchCatering at Catering
12:00
60m
Lunch
Wednesday lunch
Catering

13:00 - 14:30
Contracts and SessionsResearch Papers at L1
Chair(s): Matthew FlattUniversity of Utah
13:00
22m
Talk
Chaperone Contracts for Higher-Order Sessions
Research Papers
Hernan MelgrattiUniversity of Buenos Aires, Argentina, Luca PadovaniUniversity of Turin, Italy
DOI
13:22
22m
Talk
Whip: Higher-Order Contracts for Modern Services
Research Papers
Lucas WayeHarvard University, USA, Christos DimoulasHarvard University, USA, Stephen ChongHarvard University, USA
DOI
13:45
22m
Talk
Manifest Sharing with Session Types
Research Papers
Stephanie BalzerCarnegie Mellon University, USA, Frank PfenningCarnegie Mellon University, USA
DOI
14:07
22m
Talk
Gradual Session Types
Research Papers
Atsushi IgarashiKyoto University, Japan, Peter ThiemannUniversity of Freiburg, Germany, Vasco VasconcelosUniversity of Lisbon, Portugal, Philip WadlerUniversity of Edinburgh, UK
DOI
14:30 - 15:00
Wednesday coffee break 2Catering at Catering
14:30
30m
Coffee break
Wednesday coffee break 2
Catering

15:00 - 16:10
Integrating Static and Dynamic TypingResearch Papers at L1
Chair(s): Ronald GarciaUniversity of British Columbia
15:00
23m
Talk
Theorems for Free for Free: Parametricity, With and Without Types
Research Papers
Amal AhmedNortheastern University, USA, Dustin JamnerNortheastern University, USA, Jeremy G. SiekIndiana University, USA, Philip WadlerUniversity of Edinburgh, UK
DOI
15:23
23m
Talk
On Polymorphic Gradual Typing
Research Papers
Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan
DOI
15:46
23m
Talk
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France
DOI
16:10 - 16:40
Wednesday coffee break 3Catering at Catering
16:10
30m
Coffee break
Wednesday coffee break 3
Catering

16:40 - 17:50
Inference and AnalysisResearch Papers at L1
Chair(s): Mark JonesPortland State University
16:40
23m
Talk
Constrained Type Families
Research Papers
J. Garrett MorrisUniversity of Kansas, USA, Richard A. EisenbergBryn Mawr College, USA
DOI
17:03
23m
Talk
Automating Sized-Type Inference for Complexity Analysis
Research Papers
Martin AvanziniUniversity of Innsbruck, Austria, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France
DOI
17:26
23m
Talk
Inferring Scope through Syntactic Sugar
Research Papers
Justin PombrioBrown University, USA, Shriram KrishnamurthiBrown University, USA, Mitchell WandNortheastern University, USA
DOI
17:10 - 17:20
Termination and Complexity Competition 2017FSCD at L2
17:10
10m
Other
Termination and Complexity Competition 2017
FSCD
17:20 - 18:10
FSCD General MeetingFSCD at L2
17:20
50m
Meeting
FSCD General Meeting
FSCD

17:50 - 18:00
SRC AwardsStudent Research Competition at L1
Chair(s): Ilya SergeyUniversity College London
17:50
10m
Awards
Student Research Competition Awards
Student Research Competition
S: Ilya SergeyUniversity College London
18:00 - 18:20
Wednesday Closing EventsKeynotes and Reports at L1
18:00
10m
Talk
Program Chair's Report
Keynotes and Reports
P: Mark JonesPortland State University
18:10
10m
Talk
ICFP 2018 Announcement
Keynotes and Reports
I: Robby FindlerNorthwestern University, USA
18:30 - 22:30
18:30
4h
Social Event
Banquet
Social Events

Conference Day
Thu 7 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Session 15FSCD at L2
09:00
60m
Talk
Type systems for the relational verification of higher order programs
FSCD
A: Marco GaboardiUniversity at Buffalo, SUNY, USA
09:00 - 09:05
WelcomeML at L3
Chair(s): Sam LindleyUniversity of Edinburgh, UK
09:00
5m
Day opening
Welcome
ML

09:00 - 09:10
Welcome to FHPC'17FHPC at L4
09:00
10m
Day opening
Welcome to FHPC'17
FHPC
Phil TrinderUniversity of Glasgow, Cosmin OanceaDIKU, University of Copenhagen
09:00 - 10:00
CUFP Tutorials C2CUFP at L5
Chair(s): Runhang LiTwitter, Inc
09:00
60m
Other
Tutorial C2: Extensible Effects: understanding them, implementing them, using them
CUFP
09:00 - 10:00
CUFP Tutorials C1CUFP at L6
Chair(s): Runhang LiTwitter, Inc
09:00
60m
Other
Tutorial C1: Online Applications with Incremental
CUFP
T: Yaron Minsky, T: Sebastian FunkJane Street
09:05 - 10:00
Invited talkML at L3
Chair(s): Sam LindleyUniversity of Edinburgh, UK
09:05
55m
Talk
State machines all the way down
ML
Edwin BradyUniversity of St. Andrews, UK
09:10 - 10:10
First KeynoteFHPC at L4
Chair(s): Kevin HammondUniversity of St. Andrews, UK
09:10
60m
Talk
Haskell in the Datacentre
FHPC
Simon MarlowFacebook
10:00 - 10:30
Thursday coffee break 1Catering at Catering
10:00
30m
Coffee break
Thursday coffee break 1
Catering

10:30 - 11:59
Session 16FSCD at L2
10:30
30m
Talk
Arrays and References in Resource Aware ML
FSCD
A: Benjamin Lichtman, A: Jan HoffmannCarnegie Mellon University
11:00
30m
Talk
The Complexity of Principal Inhabitation
FSCD
A: Andrej DudenhefnerTechnical University Dortmund, A: Jakob RehofTechnical University Dortmund
11:30
29m
Talk
Types as Resources for Classical Natural Deduction
FSCD
A: Delia KesnerIRIF, France / University of Paris Diderot, France, A: Pierre Vial
10:30 - 11:45
Types and modulesML at L3
10:30
25m
Talk
Mergeable types
ML
Gowtham KakiPurdue University, KC SivaramakrishnanUniversity of Cambridge, Samodya AbeysiriwardanePurdue University, Suresh JagannathanPurdue University
10:55
25m
Talk
Tierless modules
ML
Gabriel RadanneUniversité Denis Diderot Paris 7, PPS, Jérôme VouillonUniv Paris Diderot, Sorbonne Paris Cité, BeSport
11:20
25m
Talk
First-class subtypes
ML
Jeremy YallopUniversity of Cambridge, UK, Stephen Dolan
10:30 - 11:30
CompilationFHPC at L4
Chair(s): Phil TrinderUniversity of Glasgow
10:30
30m
Talk
From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation
FHPC
A: Geoffrey MainlandDrexel University, USA, A: Siddhanathan ShanmugamDrexel University, USA
11:00
30m
Talk
Destination-Passing Style for Efficient Memory Management
FHPC
A: Amir ShaikhhaEPFL, Switzerland, A: Andrew FitzgibbonMicrosoft Research, Cambridge, A: Simon Peyton JonesMicrosoft Research, Cambridge, A: Dimitrios VytiniotisMicrosoft Research, Cambridge
10:30 - 11:30
CUFP Tutorials C1CUFP at L6
10:30
60m
Talk
Tutorial C1: Online Applications with Incremental (part 2)
CUFP
T: Yaron Minsky, T: Sebastian FunkJane Street
11:20 - 12:00
Thursday coffee break 2Catering at Catering
11:20
40m
Coffee break
Thursday coffee break 2
Catering

12:00 - 12:30
Day 1, Session 3Haskell at L1
12:00
30m
Talk
Ode on a Random Urn (Functional Pearl)
Haskell
12:00 - 12:25
VerificationML at L3
12:00
25m
Talk
VOCAL -- a verified OCAml Library
ML
Arthur CharguéraudInria, Jean-Christophe FilliatreCNRS, Paris, France, Mário PereiraLRI - Université Paris-Sud, François PottierInria, France
12:00 - 12:30
ToolsFHPC at L4
Chair(s): Cosmin OanceaDIKU, University of Copenhagen
12:00
30m
Talk
VisPar: Visualising dataflow graphs from the Par monad
FHPC
A: Maximilian AlgehedChalmers University of Technology, Sweden, A: Patrik JanssonChalmers University of Technology
12:00 - 12:30
CUFP Tutorials C1CUFP at L6
12:00
30m
Talk
Tutorial C1: Online Applications with Incremental (part 3)
CUFP
T: Yaron Minsky, T: Sebastian FunkJane Street
12:25 - 14:00
Thursday lunchCatering at Catering
12:25
1h35m
Lunch
Thursday lunch
Catering

14:00 - 15:15
Programming language designML at L3
14:00
25m
Talk
Typer: an infix statically typed Lisp
ML
Pierre DelaunayUniversité de Montréal, Vincent Archambault-BouffardUniversité de Montréal, Stefan MonnierUniversité de Montréal
14:25
25m
Talk
Relational conversion for OCaml
ML
Petr LozovSain Petersburg State University, SPbGU, Dmitri Boulytchev
14:50
25m
Talk
Towards abductive functional programming
ML
Koko MuroyaUniversity of Birmingham, UK
14:00 - 15:00
Parallel ProgrammingFHPC at L4
Chair(s): Geoffrey MainlandDrexel University, USA
14:00
30m
Talk
In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions
FHPC
A: Adam Barwell, A: Kevin HammondUniversity of St. Andrews, UK
14:30
30m
Talk
Strategies for Regular Segmented Reductions on GPU
FHPC
A: Rasmus Wriedt LarsenDIKU, University of Copenhagen, A: Troels HenriksenDIKU, University of Copenhagen
14:00 - 15:00
CUFP Tutorials C3CUFP at L5
Chair(s): Runhang LiTwitter, Inc
14:00
60m
Other
Tutorial C3: Concurrent Programming with Effect Handlers
CUFP
T: Daniel HillerströmThe University of Edinburgh, T: KC SivaramakrishnanUniversity of Cambridge
14:00 - 15:00
CUFP Tutorials C4CUFP at L6
Chair(s): Runhang LiTwitter, Inc
14:00
60m
Talk
Tutorial C4: Git under the hood with OCaml
CUFP
14:50 - 15:30
Thursday coffee break 3Catering at Catering
14:50
40m
Coffee break
Thursday coffee break 3
Catering

15:30 - 16:30
Day 1, Session 5Haskell at L1
15:30
30m
Talk
Using Coq to Write Fast and Correct Haskell
Haskell
16:00
30m
Talk
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Haskell
Niki VazouUniversity of Maryland, Leonidas LampropoulosUniversity of Pennsylvania, Jeff Polakow
15:30 - 16:20
PerformanceML at L3
15:30
25m
Talk
Making SML# a general-purpose high-performance language
ML
Atsushi OhoriTohoku University, Japan, Kenjiro TauraThe University of Tokyo, Katsuhiro UenoTohoku University
15:55
25m
Talk
Efficient representation of large, dynamic sequences in ML
ML
15:30 - 16:30
Demo SessionFHPC at L4
Chair(s): Cosmin OanceaDIKU, University of Copenhagen
15:30
29m
Demonstration
Futhark Demo
FHPC
Troels HenriksenDIKU, University of Copenhagen
16:00
29m
Demonstration
ParaFormance Demo: Democratizing Parallel Software Development
FHPC
Christopher BrownUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK
16:30
20m
Social Event
Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine
FHPC

15:30 - 16:20
CUFP Tutorials C3CUFP at L5
15:30
50m
Talk
Tutorial C3: Concurrent Programming with Effect Handlers (part 2)
CUFP
T: Daniel Hillerström, T: KC SivaramakrishnanUniversity of Cambridge
15:30 - 16:20
CUFP Tutorials C4CUFP at L6
15:30
50m
Talk
Tutorial C4: Git under the hood with OCaml (part 2)
CUFP
16:20 - 16:50
Thursday coffee break 4Catering at Catering
16:20
30m
Coffee break
Thursday coffee break 4
Catering

16:50 - 17:50
Day 1, Session 6Haskell at L1
16:50
30m
Talk
A Meta-EDSL for Distributed Web Applications
Haskell
Anton EkbladChalmers University of Technology
17:20
30m
Talk
Composable Network Stacks and Remote Monads
Haskell
16:50 - 17:40
EffectsML at L3
16:50
25m
Talk
Effects without monads: non-determinism
ML
17:15
25m
Talk
Effectively tackling the awkward squad
ML
Stephen Dolan, Spiros EliopoulosJane Street Group, Daniel HillerströmThe University of Edinburgh, Anil MadhavapeddyOCaml Labs, KC SivaramakrishnanUniversity of Cambridge, Leo WhiteJane Street
16:50 - 17:50
Demo and PanelFHPC at L4
Chair(s): Phil TrinderUniversity of Glasgow
16:50
30m
Demonstration
Ziria Demo: Wringing performance from high-level code
FHPC
Siddhanathan ShanmugamDrexel University, USA, Geoffrey MainlandDrexel University, USA
17:20
30m
Day closing
Panel Discussion: The challenges for Functional High Performance Computing
FHPC
Geoffrey MainlandDrexel University, USA, Kevin HammondUniversity of St. Andrews, UK, Simon MarlowFacebook
16:50 - 17:30
CUFP Tutorials C3CUFP at L5
16:50
40m
Talk
Tutorial C3: Concurrent Programming with Effect Handlers (part 3)
CUFP
T: Daniel HillerströmThe University of Edinburgh, T: KC SivaramakrishnanUniversity of Cambridge
16:50 - 17:30
CUFP Tutorials C4CUFP at L6
16:50
40m
Talk
Tutorial C4: Git under the hood with OCaml (part 3)
CUFP
18:15 - 20:30
Industry ReceptionSocial Events at Ashmolean Museum
18:15
2h15m
Social Event
Industry Reception
Social Events

Conference Day
Fri 8 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Day 2, Session 1Haskell at L1
09:00
60m
Talk
Algorithmic Music in Haskell (Invited Talk)
Haskell
Donya QuickStevens Institute of Technology
09:00 - 09:10
OpeningOCaml at L3
09:00
5m
Day opening
Opening
OCaml
Gabriel SchererNortheastern University
09:00 - 09:10
Opening & WelcomeErlang at L4
09:00
10m
Day opening
Opening & Welcome
Erlang

09:00 - 10:00
CUFP Tutorials C6CUFP at L5
Chair(s): Runhang LiTwitter, Inc
09:00
60m
Talk
Tutorial C6: Transducers in Practice
CUFP
09:00 - 10:00
CUFP Tutorials C5CUFP at L6
Chair(s): Runhang LiTwitter, Inc
09:00
60m
Talk
Tutorial C5: Teaching Functional Programming
CUFP
Michael SperberActive Group GmbH
09:10 - 10:10
Talk session 1OCaml at L3
09:05
35m
Talk
Invited talk: new contributors
OCaml
09:40
25m
Talk
The State of the OCaml Platform: September 2017
OCaml
09:10 - 10:00
Keynote Invited TalkErlang at L4
09:10
50m
Talk
Keynote
Erlang
10:00 - 10:30
Friday coffee break 1Catering at Catering
10:00
30m
Coffee break
Friday coffee break 1
Catering

10:30 - 11:30
Day 2, Session 2Haskell at L1
10:30
30m
Talk
Well-Typed Music Does Not Sound Wrong (Experience Report)
Haskell
Dmitrij Szamozvancev, Michael GaleUniversity of Warwick, UK
11:00
30m
Talk
Back to the Future: Time Travel in FRP
Haskell
Ivan PerezUniversity of Nottingham, UK
10:30 - 11:30
Talk session 2OCaml at L3
10:30
20m
Talk
Owl: A General-Purpose Numerical Library in OCaml
OCaml
Liang WangUniversity of Cambridge
Link to publication Pre-print
10:50
20m
Talk
Extending OCaml's open
OCaml
Runhang LiTwitter, Inc, Jeremy YallopUniversity of Cambridge, UK
Link to publication Pre-print
11:10
20m
Talk
Genspio: Generating Shell Phrases In OCaml
OCaml
Sebastien MondetMount Sinai - Hammer Lab
Pre-print
10:30 - 11:30
CUFP Tutorials C6CUFP at L5
10:30
60m
Talk
Tutorial C6: Transducers in Practice (part 2)
CUFP
T: Renzo BorgattiuSwitch
10:30 - 11:30
CUFP Tutorials C5CUFP at L6
10:30
60m
Talk
Tutorial C5: Teaching Functional Programming (part 2)
CUFP
T: Michael SperberActive Group GmbH
11:20 - 12:00
Friday coffee break 2Catering at Catering
11:20
40m
Coffee break
Friday coffee break 2
Catering

12:00 - 12:30
Day 2, Session 3Haskell at L1
12:00
30m
Talk
The Linearity Monad
Haskell
Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
12:00 - 12:25
Session 3Erlang at L4
12:00
25m
Talk
Erlang and Elixir development news
Erlang

12:00 - 12:30
CUFP Tutorials C6CUFP at L5
12:00
30m
Talk
Tutorial C6: Transducers in Practice (part 3)
CUFP
T: Renzo BorgattiuSwitch
12:00 - 12:30
CUFP Tutorials C5CUFP at L6
12:00
30m
Talk
Tutorial C5: Teaching Functional Programming (part 3)
CUFP
T: Michael SperberActive Group GmbH
12:25 - 14:00
Friday lunchCatering at Catering
12:25
1h35m
Lunch
Friday lunch
Catering

14:00 - 15:00
Day 2, Session 4Haskell at L1
14:00
30m
Talk
Elaboration on Functional Dependencies
Haskell
Georgios KarachaliasKU Leuven, Belgium, Tom SchrijversKU Leuven
14:30
30m
Talk
Quantified Class Constraints
Haskell
Gert-Jan Bottu, Georgios KarachaliasKU Leuven, Belgium, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, China, Philip WadlerUniversity of Edinburgh, UK
14:00 - 14:50
Session 4Erlang at L4
14:00
25m
Talk
Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang
Erlang
Kagumi AzumaKwansei Gakuin University, Nagisa IshiuraKwansei Gakuin University, Nobuaki YoshidaASTEM RI/KYOTO, Hiroyuki KanbaraASTEM RI/KYOTO
14:25
25m
Talk
Structuring Erlang BEAM control flow
Erlang
Dániel LukácsEötvös Loránd University, Melinda Tóth
14:00 - 15:00
CUFP Tutorials C8CUFP at L5
Chair(s): Runhang LiTwitter, Inc
14:00
60m
Talk
Tutorial C8: GraphQL Servers in OCaml
CUFP
T: Andreas GarnæsZendesk
14:00 - 15:00
CUFP Tutorials C7CUFP at L6
Chair(s): Runhang LiTwitter, Inc
14:00
60m
Talk
Tutorial C7: Owl - Data Science in OCaml
CUFP
T: Liang WangUniversity of Cambridge
14:50 - 15:30
Friday coffee break 3Catering at Catering
14:50
40m
Coffee break
Friday coffee break 3
Catering

15:30 - 16:30
Day 2, Session 5Haskell at L1
15:30
30m
Talk
Hardware Software Co-Design in Haskell
Haskell
16:00
30m
Talk
Streaming Irregular Arrays
Haskell
Robert Clifton-Everest, Trevor L. McDonellUniversity of New South Wales, Australia, Manuel Chakravarty, Gabriele KellerData61,CSIRO (formerly NICTA) and UNSW
15:30 - 16:30
Talk session 4OCaml at L3
15:30
20m
Talk
A B-tree library for OCaml
OCaml
Tom RidgeUniversity of Leicester, UK
Link to publication
15:50
20m
Talk
Wodan: a pure OCaml, flash-aware filesystem library
OCaml
Link to publication
16:10
20m
Talk
Tezos: the OCaml Crypto-Ledger
OCaml
Benjamin CanouOCamlPro, n.n., Grégoire HenryOCamlPro, n.n., Pierre ChambartOCamlPRO, Fabrice Le FessantOCamlPro, Arthur BREITMANDynamic Ledger Solutions
15:30 - 16:20
CUFP Tutorials C8CUFP at L5
15:30
50m
Talk
Tutorial C8: GraphQL Servers in OCaml (part 2)
CUFP
T: Andreas GarnæsZendesk
15:30 - 16:20
CUFP Tutorials C7CUFP at L6
15:30
50m
Talk
Tutorial C7: Owl - Data Science in OCaml (part 2)
CUFP
T: Liang WangUniversity of Cambridge
16:20 - 16:50
Friday coffee break 4Catering at Catering
16:20
30m
Coffee break
Friday coffee break 4
Catering

16:50 - 17:40
Talk session 5OCaml at L3
17:00
20m
Talk
Component-based Program Synthesis in OCaml
OCaml
Zhanpeng LiangUniversity of Southern California, Kanae Tsushima
Link to publication
17:20
20m
Talk
Testing with Crowbar
OCaml
16:50 - 17:50
Session 6Erlang at L4
16:50
30m
Talk
eAOP - An Aspect Oriented Programming Framework for Erlang
Erlang
Ian CassarUniversity of Malta, Adrian FrancalanzaUniversity of Malta, Luca AcetoReykjavik University, Anna IngolfsdottirReykjavik University
17:20
30m
Talk
In medias res: WIP discussion
Erlang

16:50 - 17:30
CUFP Tutorials C8CUFP at L5
16:50
40m
Talk
Tutorial C8: GraphQL Servers in OCaml (part 3)
CUFP
T: Andreas GarnæsZendesk
16:50 - 17:30
CUFP Tutorials C7CUFP at L6
16:50
40m
Talk
Tutorial C7: Owl - Data Science in OCaml (part 3)
CUFP
T: Liang WangUniversity of Cambridge

Conference Day
Sat 9 Sep

Displayed time zone: Belfast change

09:00 - 10:10
State of GHCHIW at L1
Chair(s): Richard A. EisenbergBryn Mawr College, USA
09:00
30m
Talk
Progress on GHC
HIW
Simon Peyton JonesMicrosoft Research, Cambridge
09:30
30m
Talk
GHC Infrastructure Update and Discussion
HIW
Ben GamariWell-Typed LLP
10:00
10m
Talk
Getting Ready for Hadrian
HIW
Andrey Mokhov, Zhen ZhangUniversity of Washington, Ben GamariWell-Typed LLP, Neil Mitchell
09:00 - 09:10
IntroductionFARM at L3
09:00
10m
Day opening
Welcome
FARM
C: Michael SperberActive Group GmbH, P: Jean BressonUMR STMS: IRCAM-CNRS-UPMC
09:10 - 10:00
CUFP Talks 1CUFP at L2
09:10
25m
Talk
Keynote: Are We There Yet?
CUFP
Bodil StokkeChurch of Emacs
09:35
25m
Talk
Bonsai: a DSL for serverless firm real-time decisioning
CUFP
10:00 - 10:30
Saturday coffee break 1Catering at Catering
10:00
30m
Coffee break
Saturday coffee break 1
Catering

10:30 - 11:30
Compiling to LLVMHIW at L1
Chair(s): Jan StolarekUniversity of Edinburgh, UK
10:30
25m
Talk
Native Support for Explicit Stacks in LLVM
HIW
Kavon FarvardinUniversity of Chicago, Simon Peyton JonesMicrosoft Research, Cambridge
10:55
25m
Talk
SimplexHC: Lowering High-Level Haskell to Imperative IR
HIW
Siddharth BhatIIT Hyderabad
11:20
10m
Talk
Lightning Talk Slot #1
HIW

10:30 - 11:30
Session 2: Papers/DemosFARM at L3
Chair(s): Ivan PerezUniversity of Nottingham, UK
10:30
20m
Demonstration
Demo — African Polyphony and Polyrhythm
FARM
Chris FordThoughtWorks (UK) Ltd.
Pre-print
10:50
20m
Demonstration
Demo — Vivid: Sound Synthesis with Haskell and SuperCollider
FARM
Pre-print
11:10
30m
Talk
GALE: A Functional Graphic Adventure Library and Engine
FARM
Ivan PerezUniversity of Nottingham, UK
11:20 - 12:00
Saturday coffee break 2Catering at Catering
11:20
40m
Coffee break
Saturday coffee break 2
Catering

12:00 - 12:25
ConstraintsHIW at L1
Chair(s): Ben GamariWell-Typed LLP
12:00
25m
Talk
On Unsatisfiability
HIW
J. Garrett MorrisUniversity of Kansas, USA
12:00 - 12:25
CUFP Talks 3CUFP at L2
12:00
25m
Talk
Gens N' Roses: Appetite for Reduction
CUFP
12:25 - 14:00
Saturday lunchCatering at Catering
12:25
1h35m
Lunch
Saturday lunch
Catering

14:00 - 15:00
Working in CoreHIW at L1
Chair(s): Adam GundryWell-Typed LLP
14:00
25m
Talk
Why GHC Core and Linear Logic Should be Best Friends
HIW
14:25
25m
Talk
Demand Analysis vs. Call Arity
HIW
Sebastian GrafKarlsruhe Institute of Technology
14:50
10m
Talk
Lightning Talk Slot #2
HIW

14:00 - 14:50
CUFP Talks 4CUFP at L2
14:00
25m
Talk
Formally Verifying a Smart-Contract Language Implementation with Isabelle
CUFP
Simon MeierDigital Asset
14:25
25m
Talk
Haskell games and apps for iOS and Android
CUFP
Ivan PerezUniversity of Nottingham, UK
14:00 - 15:00
Session 4: TutorialFARM at L3
Chair(s): Jean BressonUMR STMS: IRCAM-CNRS-UPMC
14:00
60m
Talk
FAUST Tutorial for Functional Programmers
FARM
14:50 - 15:30
Saturday coffee break 3Catering at Catering
14:50
40m
Coffee break
Saturday coffee break 3
Catering

15:30 - 16:30
Tool SupportHIW at L1
Chair(s): Wren RomanoX
15:30
25m
Talk
IDE Support in GHC
HIW
15:55
25m
Talk
Tracking GHC Performance
HIW
16:20
10m
Talk
Lightning Talk Slot #3
HIW

15:30 - 16:20
CUFP Talks 5CUFP at L2
15:30
25m
Talk
Using Haskell to run a datacenter
CUFP
15:55
25m
Talk
Functional Facades over Legacy Code
CUFP
Nicholas CowleG-Research, Robin KayG-Research
15:30 - 16:20
Session 5: DemosFARM at L3
Chair(s): David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
15:30
20m
Demonstration
Demo — The Arpeggigon: A Functional Reactive Musical Automaton
FARM
Henrik NilssonUniversity of Nottingham, UK
Pre-print
15:50
20m
Demonstration
Demo — Ait: A Concatenative Language for Creative Programming
FARM
Pre-print
16:20 - 16:50
Saturday coffee break 4Catering at Catering
16:20
30m
Coffee break
Saturday coffee break 4
Catering

16:50 - 17:50
All Broken UpHIW at L1
Chair(s): Bartosz NitkaFacebook
16:50
25m
Talk
An Experiment in Fragment-Based Code Distribution
HIW
Philipp SchusterUniversity of Tübingen
17:15
35m
Talk
Lightning Talk Slot #4
HIW

16:50 - 17:40
Session 6: Papers/DemosFARM at L3
Chair(s): Henrik NilssonUniversity of Nottingham, UK
16:50
30m
Talk
Unified Media Programming: An Algebraic Approach
FARM
Simon ArchipoffCNRS LaBRI, Inria Bordeaux,, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
17:20
20m
Demonstration
Demo — Octopus: A High-Level Fast 3D Animation Language
FARM
Simon ArchipoffCNRS LaBRI, Inria Bordeaux,, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
Pre-print
19:30 - 22:00
FARM Performance EveningSocial Events at Old Fire Station
19:30
2h30m
Social Event
FARM Evening Of Algorithmic Arts
Social Events