Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
VenueMathematical Institute
Room nameL1
Floor0
Capacity360
Room InformationNo extra information available
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: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
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
12:00 - 12:30
Session 2PLMW at L1
12:00
30m
Talk
Not How To Do Your PhD
PLMW
Gabriel SchererNortheastern University
File Attached
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
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

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: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
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
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
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

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: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
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
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
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: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
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
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: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: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

Conference Day
Thu 7 Sep

Displayed time zone: Belfast change

12:00 - 12:30
Day 1, Session 3Haskell at L1
12:00
30m
Talk
Ode on a Random Urn (Functional Pearl)
Haskell
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
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

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
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
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
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
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

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
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

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
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

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

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

Conference Day
Sun 3 Sep

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
L1

Conference Day
Thu 7 Sep

Displayed time zone: Belfast change

Conference Day
Fri 8 Sep

Displayed time zone: Belfast change

Conference Day
Sat 9 Sep

Displayed time zone: Belfast change

Conference Day
Sun 3 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
L1
PLMW
Welcome
09:00 - 09:10
PLMW
Keynote
09:10 - 10:00
PLMW
Gradual Typing
14:00 - 14:30

Conference Day
Mon 4 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L1

Conference Day
Wed 6 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L1

Conference Day
Sat 9 Sep

Displayed time zone: Belfast change