Conference Dates
Conference Dates are in time zone (GMT+01:00) Greenwich Mean Time : Belfast, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Sun 3 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sun 3 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 09:10 Talk | Welcome PLMW Brigitte PientkaMcGill University, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Dan LicataWesleyan University |
09:00 - 09:05 Day opening | Welcome TyDe |
09:00 - 09:10 Day opening | Welcome HOPE |
09:00 - 10:00 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 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 - 10:00 Talk | Keynote PLMW Chris MartensNorth Carolina State University |
09:10 - 10:10 Talk | Invited Talk: Semantics of Effect Systems by Graded Monads HOPE Shin-ya KatsumataNational Institute of Informatics |
09:10 - 10:10 Talk | Keynote Scheme Sam Tobin-HochstadtIndiana University |
10:00 - 10:30 Coffee break | Sunday coffee break 1 Catering |
10:30 - 11:00 Talk | A Few Frank Remarks PLMW | ||
11:00 - 11:30 Talk | Compositional Compiler Correctness PLMW Amal AhmedNortheastern University, USA File Attached |
10:30 - 11:00 Talk | Generic packet descriptions: verified parsing and pretty printing of low-level data TyDe | ||
11:00 - 11:30 Talk | Structured asynchrony with algebraic effects TyDe Daan LeijenMicrosoft Research |
10:30 - 11:00 Talk | Higher-order Programming is an Effect HOPE File Attached | ||
11:00 - 11:30 Talk | A monadic solution to the Cartwright-Felleisen-Wadler conjecture HOPE File Attached |
10:30 - 11:15 Talk | Paper: Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation Scheme Satoshi EgiRakuten Institute of Technology | ||
11:15 - 11:30 Talk | Lightning Talk: Extending the LISP model from cons cells to triples, from trees to hypergraphs Scheme |
10:30 - 11:30 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 Coffee break | Sunday coffee break 2 Catering |
12:00 - 12:30 Talk | Not How To Do Your PhD PLMW Gabriel SchererNortheastern University File Attached |
12:00 - 12:25 Talk | Cogent⇑: giving systems engineers a stepping stone TyDe Zilin ChenUNSW, Australia |
12:00 - 12:30 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 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 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 Lunch | Sunday lunch Catering |
14:00 - 14:30 Talk | Gradual Typing PLMW Ronald GarciaUniversity of British Columbia File Attached | ||
14:30 - 15:00 Talk | Scala: Types in Theory & Practice PLMW Nada AminUniversity of Cambridge File Attached |
14:00 - 14:30 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 - 15:00 Talk | Type-directed diffing of structured data TyDe Victor Cacciari MiraldoUniversity of Utrecht, Pierre-Evariste DagandLIP6/CNRS , Wouter SwierstraUniversity of Utrecht |
14:00 - 14:30 Talk | Handling fibred algebraic effects HOPE Danel AhmanUniversity of Edinburgh | ||
14:30 - 15:00 Talk | Only Control Effects and Dependent Types HOPE |
14:00 - 14:45 Talk | Paper: Toward Parallelizing Control-flow Analysis with Datalog Scheme | ||
14:45 - 15:00 Talk | Lightning: Gerbil on Gambit, as they say Racket on Chez Scheme |
14:00 - 15:00 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 Coffee break | Sunday coffee break 3 Catering |
15:30 - 16:30 Talk | How to Write Papers and Give Talks That People Can Follow PLMW Derek DreyerMPI-SWS Media Attached |
15:30 - 15:55 Talk | Affine killing TyDe | ||
15:55 - 16:20 Talk | On ringads and foldables TyDe James McKinnaUniversity of Edinburgh |
15:30 - 16:00 Talk | Programming a Web Server with Algebraic Effects HOPE Daan LeijenMicrosoft Research | ||
16:00 - 16:30 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:15 Talk | Report: Status of the ongoing R7RS standardization process Scheme | ||
16:15 - 16:30 Talk | Lightning: {lambda talk} Scheme |
15:30 - 16:20 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 Coffee break | Sunday coffee break 4 Catering |
16:50 - 17:40 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:15 Talk | Type oriented programming for task based parallelism TyDe | ||
17:15 - 17:40 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:20 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:40 Talk | Invited Talk Scheme Matthew MightUniversity of Utah, USA | ||
17:40 - 17:50 Day closing | Goodbye Scheme |
16:50 - 17:50 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 |
Mon 4 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Mon 4 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00: Monday KeynoteKeynotes and Reports at L1 Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford | |||
09:00 - 10:00 Talk | Compositional creativity: some principles for talking to computersKeynote Keynotes and Reports |
10:00 - 10:30 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 - 10:52 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 - 11:15 Talk | Testing and Debugging Functional Reactive Programming Research Papers DOI | ||
11:15 - 11:37 Talk | Lock-Step Simulation Is Child's Play (Experience Report) Research Papers DOI | ||
11:37 - 12:00 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 Other | Welcome message FSCD |
10:45 - 11:45 Talk | Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages FSCD |
12:00 - 13:00 Lunch | Monday lunch Catering |
13:00 - 14:30: Functional Programming TechniquesResearch Papers at L1 Chair(s): Graham HuttonUniversity of Nottingham | |||
13:00 - 13:22 Talk | Faster Coroutine Pipelines Research Papers Mike SpiveyUniversity of Oxford, UK DOI | ||
13:22 - 13:45 Talk | A Pretty But Not Greedy Printer (Functional Pearl) Research Papers Jean-Philippe BernardyUniversity of Gothenburg DOI | ||
13:45 - 14:07 Talk | Generic Functional Parallel Algorithms: Scan and FFT Research Papers Conal ElliottTarget, USA DOI | ||
14:07 - 14:30 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 |
13:00 - 13:30 Talk | Polynomial running times for polynomial-time oracle machines FSCD | ||
13:30 - 14:00 Talk | A Curry-Howard Approach to Church’s Synthesis FSCD | ||
14:00 - 14:30 Talk | Streett Automata Model Checking of Higher-Order Recursion Schemes FSCD A: Ryota Suzuki, A: Koichi Fujima, A: Naoki KobayashiUniversity of Tokyo, Japan, A: Takeshi TsukadaUniversity of Tokyo, Japan |
14:30 - 15:00 Coffee break | Monday coffee break 2 Catering |
15:00 - 15:23 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 - 15:46 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 - 16:10 Talk | Symbolic Conditioning of Arrays in Probabilistic Programs Research Papers DOI |
15:00 - 15:30 Talk | Relating System F and λ2: A Case Study in Coq, Abella and Beluga FSCD | ||
15:30 - 16:00 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 Coffee break | Monday coffee break 3 Catering |
16:40 - 17:02 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 - 17:25 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 - 17:47 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 - 18:10 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 |
16:40 - 17:10 Talk | A polynomial-time algorithm for the Lambek calculus with brackets of bounded order FSCD | ||
17:10 - 17:40 Talk | A sequent calculus for semi-associativity FSCD | ||
17:40 - 18:10 Talk | Combinatorial Flows and their Normalisation FSCD |
18:10 - 18:20: Monday Closing EventsKeynotes and Reports at L1 Chair(s): Peter ThiemannUniversity of Freiburg, Germany | |||
18:10 - 18:20 Day closing | Monday Announcements Keynotes and Reports |
18:30 - 20:30 Social Event | Welcome Reception Social Events |
Tue 5 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Tue 5 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00: Tuesday KeynoteKeynotes and Reports at L1 Chair(s): Mark JonesPortland State University | |||
09:00 - 10:00 Talk | Assuring AIKeynote Keynotes and Reports |
10:00 - 10:30 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 - 10:52 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 - 11:15 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 - 11:37 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 - 12:00 Talk | Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols Research Papers Geoffrey MainlandDrexel University, USA DOI |
10:30 - 11:30 Talk | Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses FSCD Georg MoserUniversity of Innsbruck |
11:30 - 12:00 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 Lunch | Tuesday lunch Catering |
13:00 - 14:30: Foundations of Higher-Order ProgrammingResearch Papers at L1 Chair(s): Gabriel SchererNortheastern University | |||
13:00 - 13:22 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 - 13:45 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 - 14:07 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 - 14:30 Talk | No-Brainer CPS Conversion Research Papers Milo DavisNortheastern University, USA, William MeehanNortheastern University, USA, Olin ShiversNortheastern University, USA DOI |
14:30 - 15:00 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 - 15:23 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 - 15:46 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 - 16:10 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 - 15:30 Talk | Is the optimal implementation inefficient? Elementarily not FSCD | ||
15:30 - 16:00 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 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 - 17:03 Talk | Compiling to Categories Research Papers Conal ElliottTarget, USA DOI | ||
17:03 - 17:26 Talk | Visitors Unchained Research Papers François PottierInria, France DOI | ||
17:26 - 17:50 Talk | Staged Generic Programming Research Papers Jeremy YallopUniversity of Cambridge, UK DOI Pre-print |
16:40 - 17:10 Talk | Generalized Refocusing: from Hybrid Strategies to Abstract Machines FSCD | ||
17:10 - 17:40 Talk | Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or FSCD | ||
17:40 - 18:10 Talk | Refutation of Sallé's Longstanding Conjecture FSCD |
17:50 - 18:20 Talk | Programming Contest Report Keynotes and Reports |
Wed 6 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 09:37: SRC PresentationsStudent Research Competition at L1 Chair(s): Ilya SergeyUniversity College London | |||
09:00 - 09:37 Awards | Student Research Competition: Finalist Presentations Student Research Competition |
09:00 - 10:00 Talk | Quantitative semantics for probabilistic programming FSCD |
09:37 - 10:00: Domain-Specific LanguagesResearch Papers at L1 Chair(s): Martin ErwigOregon State University | |||
09:37 - 10:00 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 Coffee break | Wednesday coffee break 1 Catering |
10:30 - 12:00: Dependently Typed ProgrammingResearch Papers at L1 Chair(s): Dan LicataWesleyan University | |||
10:30 - 10:52 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 - 11:15 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 - 11:37 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 - 12:00 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 - 11:00 Talk | Displayed categories FSCD | ||
11:00 - 11:30 Talk | List Objects with Algebraic Structure FSCD | ||
11:30 - 12:00 Talk | There is only one notion of differentiation FSCD |
12:00 - 13:00 Lunch | Wednesday lunch Catering |
13:00 - 14:30: Contracts and SessionsResearch Papers at L1 Chair(s): Matthew FlattUniversity of Utah | |||
13:00 - 13:22 Talk | Chaperone Contracts for Higher-Order Sessions Research Papers DOI | ||
13:22 - 13:45 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 - 14:07 Talk | Manifest Sharing with Session Types Research Papers DOI | ||
14:07 - 14:30 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 |
13:00 - 13:30 Talk | A Fibrational Framework for Substructural and Modal Logics FSCD | ||
13:30 - 14:00 Talk | Dinaturality between syntax and semantics FSCD | ||
14:00 - 14:30 Talk | Models of Type Theory Based on Moore Paths FSCD |
14:30 - 15:00 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 - 15:23 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 - 15:46 Talk | On Polymorphic Gradual Typing Research Papers Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan DOI | ||
15:46 - 16:10 Talk | Gradual Typing with Union and Intersection Types Research Papers Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France DOI |
15:00 - 15:30 Talk | Böhm Reduction in Infinitary Term Graph Rewriting Systems FSCD | ||
15:30 - 16:00 Talk | Infinite Runs in Abstract Completion FSCD |
16:10 - 16:40 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 - 17:03 Talk | Constrained Type Families Research Papers DOI | ||
17:03 - 17:26 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 - 17:50 Talk | Inferring Scope through Syntactic Sugar Research Papers Justin PombrioBrown University, USA, Shriram KrishnamurthiBrown University, USA, Mitchell WandNortheastern University, USA DOI |
16:40 - 17:10 Talk | Negative Translations and Normal Modality FSCD |
17:10 - 17:20 Other | Termination and Complexity Competition 2017 FSCD |
17:20 - 18:10 Meeting | FSCD General Meeting FSCD |
17:50 - 18:00: SRC AwardsStudent Research Competition at L1 Chair(s): Ilya SergeyUniversity College London | |||
17:50 - 18:00 Awards | Student Research Competition Awards Student Research Competition |
18:00 - 18:10 Talk | Program Chair's Report Keynotes and Reports | ||
18:10 - 18:20 Talk | ICFP 2018 Announcement Keynotes and Reports |
18:30 - 22:30 Social Event | Banquet Social Events |
Thu 7 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Thu 7 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00 Talk | Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk) Haskell Didier RémyINRIA |
09:00 - 10:00 Talk | Type systems for the relational verification of higher order programs FSCD |
09:00 - 09:05 Day opening | Welcome ML |
09:00 - 09:10 Day opening | Welcome to FHPC'17 FHPC |
09:00 - 10:00 Other | Tutorial C2: Extensible Effects: understanding them, implementing them, using them CUFP |
09:00 - 10:00 Other | Tutorial C1: Online Applications with Incremental CUFP |
09:05 - 10:00 Talk | State machines all the way down ML Edwin BradyUniversity of St. Andrews, UK |
09:10 - 10:10 Talk | Haskell in the Datacentre FHPC Simon MarlowFacebook |
10:00 - 10:30 Coffee break | Thursday coffee break 1 Catering |
10:30 - 11:00 Talk | Algebraic Graphs with Class (Functional Pearl) Haskell | ||
11:00 - 11:30 Talk | Packrats Parse in Packs Haskell |
10:30 - 11:00 Talk | Arrays and References in Resource Aware ML FSCD | ||
11:00 - 11:30 Talk | The Complexity of Principal Inhabitation FSCD | ||
11:30 - 11:59 Talk | Types as Resources for Classical Natural Deduction FSCD |
10:30 - 10:55 Talk | Mergeable types ML Gowtham KakiPurdue University, KC SivaramakrishnanUniversity of Cambridge, Samodya AbeysiriwardanePurdue University, Suresh JagannathanPurdue University | ||
10:55 - 11:20 Talk | Tierless modules ML Gabriel RadanneUniversité Denis Diderot Paris 7, PPS, Jérôme VouillonUniv Paris Diderot, Sorbonne Paris Cité, BeSport | ||
11:20 - 11:45 Talk | First-class subtypes ML |
10:30 - 11:00 Talk | From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation FHPC | ||
11:00 - 11:30 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 Talk | Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 2) CUFP |
10:30 - 11:30 Talk | Tutorial C1: Online Applications with Incremental (part 2) CUFP |
11:20 - 12:00 Coffee break | Thursday coffee break 2 Catering |
12:00 - 12:30 Talk | Ode on a Random Urn (Functional Pearl) Haskell |
12:00 - 12:25 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 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 Talk | Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 3) CUFP |
12:00 - 12:30 Talk | Tutorial C1: Online Applications with Incremental (part 3) CUFP |
12:25 - 14:00 Lunch | Thursday lunch Catering |
14:00 - 14:30 Demonstration | QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration) Haskell Maximilian AlgehedChalmers University of Technology, Sweden, Koen ClaessenChalmers University of Technology, Moa JohanssonChalmers University of Technology, Nicholas Smallbone | ||
14:30 - 15:00 Talk | Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results Haskell |
14:00 - 14:25 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 - 14:50 Talk | Relational conversion for OCaml ML | ||
14:50 - 15:15 Talk | Towards abductive functional programming ML Koko MuroyaUniversity of Birmingham, UK |
14:00 - 14:30 Talk | In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions FHPC | ||
14:30 - 15:00 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 Other | Tutorial C3: Concurrent Programming with Effect Handlers CUFP |
14:00 - 15:00 Talk | Tutorial C4: Git under the hood with OCaml CUFP |
14:50 - 15:30 Coffee break | Thursday coffee break 3 Catering |
15:30 - 16:00 Talk | Using Coq to Write Fast and Correct Haskell Haskell | ||
16:00 - 16:30 Talk | A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq Haskell |
15:30 - 15:55 Talk | Making SML# a general-purpose high-performance language ML Atsushi OhoriTohoku University, Japan, Kenjiro TauraThe University of Tokyo, Katsuhiro UenoTohoku University | ||
15:55 - 16:20 Talk | Efficient representation of large, dynamic sequences in ML ML |
15:30 - 15:59 Demonstration | Futhark Demo FHPC Troels HenriksenDIKU, University of Copenhagen | ||
16:00 - 16:29 Demonstration | ParaFormance Demo: Democratizing Parallel Software Development FHPC | ||
16:30 - 16:50 Social Event | Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine FHPC |
15:30 - 16:20 Talk | Tutorial C3: Concurrent Programming with Effect Handlers (part 2) CUFP |
15:30 - 16:20 Talk | Tutorial C4: Git under the hood with OCaml (part 2) CUFP |
16:20 - 16:50 Coffee break | Thursday coffee break 4 Catering |
16:50 - 17:20 Talk | A Meta-EDSL for Distributed Web Applications Haskell Anton EkbladChalmers University of Technology | ||
17:20 - 17:50 Talk | Composable Network Stacks and Remote Monads Haskell |
16:50 - 17:15 Talk | Effects without monads: non-determinism ML | ||
17:15 - 17:40 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:20 Demonstration | Ziria Demo: Wringing performance from high-level code FHPC | ||
17:20 - 17:50 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 Talk | Tutorial C3: Concurrent Programming with Effect Handlers (part 3) CUFP |
16:50 - 17:30 Talk | Tutorial C4: Git under the hood with OCaml (part 3) CUFP |
18:15 - 20:30 Social Event | Industry Reception Social Events |
Fri 8 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Fri 8 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 10:00 Talk | Algorithmic Music in Haskell (Invited Talk) Haskell Donya QuickStevens Institute of Technology |
09:00 - 09:05 Day opening | Opening OCaml Gabriel SchererNortheastern University |
09:00 - 09:10 Day opening | Opening & Welcome Erlang |
09:00 - 10:00 Talk | Tutorial C6: Transducers in Practice CUFP Renzo BorgattiuSwitch |
09:00 - 10:00 Talk | Tutorial C5: Teaching Functional Programming CUFP Michael SperberActive Group GmbH |
09:05 - 09:40 Talk | Invited talk: new contributors OCaml | ||
09:40 - 10:05 Talk | The State of the OCaml Platform: September 2017 OCaml Anil MadhavapeddyOCaml Labs |
09:10 - 10:00 Talk | Keynote Erlang |
10:00 - 10:30 Coffee break | Friday coffee break 1 Catering |
10:30 - 11:00 Talk | Well-Typed Music Does Not Sound Wrong (Experience Report) Haskell | ||
11:00 - 11:30 Talk | Back to the Future: Time Travel in FRP Haskell Ivan PerezUniversity of Nottingham, UK |
10:30 - 10:50 Talk | Owl: A General-Purpose Numerical Library in OCaml OCaml Liang WangUniversity of Cambridge Link to publication Pre-print | ||
10:50 - 11:10 Talk | Extending OCaml's open OCaml Link to publication Pre-print | ||
11:10 - 11:30 Talk | Genspio: Generating Shell Phrases In OCaml OCaml Sebastien MondetMount Sinai - Hammer Lab Pre-print |
10:30 - 10:55 Talk | Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm Erlang Evgeniy ShishkinJSC "InfoTeCS" DOI File Attached | ||
10:55 - 11:20 Talk | Towards an Isabelle/HOL Formalisation of Core Erlang Erlang Joseph HarrisonUniversity of Kent |
10:30 - 11:30 Talk | Tutorial C6: Transducers in Practice (part 2) CUFP |
10:30 - 11:30 Talk | Tutorial C5: Teaching Functional Programming (part 2) CUFP |
11:20 - 12:00 Coffee break | Friday coffee break 2 Catering |
11:35 - 11:45 Talk | Flash poster presentation OCaml | ||
11:45 - 12:30 Talk | mSAT: An OCaml SAT Solver OCaml Bury GuillaumeINRIA / LSV / CNRS Link to publication | ||
11:45 - 12:30 Talk | Jbuilder: a modern approach to OCaml development OCaml | ||
11:45 - 12:30 Talk | Tyre – Typed Regular Expressions OCaml Gabriel RadanneUniversité Denis Diderot Paris 7, PPS Link to publication | ||
11:45 - 12:30 Talk | ocamli: Interpreted OCaml OCaml Link to publication |
12:00 - 12:30 Talk | The Linearity Monad Haskell |
12:00 - 12:25 Talk | Erlang and Elixir development news Erlang |
12:00 - 12:30 Talk | Tutorial C6: Transducers in Practice (part 3) CUFP |
12:00 - 12:30 Talk | Tutorial C5: Teaching Functional Programming (part 3) CUFP |
12:25 - 14:00 Lunch | Friday lunch Catering |
14:00 - 14:30 Talk | Elaboration on Functional Dependencies Haskell | ||
14:30 - 15:00 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:20 Talk | ROTOR: First Steps Towards a Refactoring Tool for OCaml OCaml Link to publication | ||
14:20 - 14:40 Talk | A memory model for multicore OCaml OCaml Link to publication | ||
14:40 - 15:00 Talk | Bioinformatics, The Typed Tagless Final Way OCaml Sebastien MondetMount Sinai - Hammer Lab Pre-print |
14:00 - 14:25 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 - 14:50 Talk | Structuring Erlang BEAM control flow Erlang |
14:00 - 15:00 Talk | Tutorial C8: GraphQL Servers in OCaml CUFP |
14:00 - 15:00 Talk | Tutorial C7: Owl - Data Science in OCaml CUFP |
14:50 - 15:30 Coffee break | Friday coffee break 3 Catering |
15:30 - 16:00 Talk | Hardware Software Co-Design in Haskell Haskell | ||
16:00 - 16:30 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 - 15:50 Talk | A B-tree library for OCaml OCaml Tom RidgeUniversity of Leicester, UK Link to publication | ||
15:50 - 16:10 Talk | Wodan: a pure OCaml, flash-aware filesystem library OCaml Gabriel de PerthuisOCaml Labs Link to publication | ||
16:10 - 16:30 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 - 15:55 Talk | The Shared-Memory Interferences of Erlang/OTP Built-ins Erlang | ||
15:55 - 16:20 Talk | Towards Change-driven Testing Erlang |
15:30 - 16:20 Talk | Tutorial C8: GraphQL Servers in OCaml (part 2) CUFP |
15:30 - 16:20 Talk | Tutorial C7: Owl - Data Science in OCaml (part 2) CUFP |
16:20 - 16:50 Coffee break | Friday coffee break 4 Catering |
16:50 - 17:20 Talk | Improving STM Performance with Transactional Structs Haskell | ||
17:20 - 17:50 Talk | Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping Haskell |
17:00 - 17:20 Talk | Component-based Program Synthesis in OCaml OCaml Link to publication | ||
17:20 - 17:40 Talk | Testing with Crowbar OCaml |
16:50 - 17:20 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 - 17:50 Talk | In medias res: WIP discussion Erlang |
16:50 - 17:30 Talk | Tutorial C8: GraphQL Servers in OCaml (part 3) CUFP |
16:50 - 17:30 Talk | Tutorial C7: Owl - Data Science in OCaml (part 3) CUFP |
Sat 9 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sat 9 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
09:00 - 09:30 Talk | Progress on GHC HIW Simon Peyton JonesMicrosoft Research, Cambridge | ||
09:30 - 10:00 Talk | GHC Infrastructure Update and Discussion HIW Ben GamariWell-Typed LLP | ||
10:00 - 10:10 Talk | Getting Ready for Hadrian HIW |
09:00 - 09:10 Day opening | Welcome FARM |
09:10 - 09:35 Talk | Keynote: Are We There Yet? CUFP Bodil StokkeChurch of Emacs | ||
09:35 - 10:00 Talk | Bonsai: a DSL for serverless firm real-time decisioning CUFP Jeremie Lasalle-RatelleAppNexus |
09:10 - 09:40 Talk | A Categorial Grammar for Music and Its Use in Automatic Melody Generation FARM | ||
09:40 - 10:00 Demonstration | Demo — Representation of Musical Notation in Haskell FARM Pre-print |
10:00 - 10:30 Coffee break | Saturday coffee break 1 Catering |
10:30 - 10:55 Talk | Native Support for Explicit Stacks in LLVM HIW | ||
10:55 - 11:20 Talk | SimplexHC: Lowering High-Level Haskell to Imperative IR HIW Siddharth BhatIIT Hyderabad | ||
11:20 - 11:30 Talk | Lightning Talk Slot #1 HIW |
10:30 - 10:55 Talk | Interfacing OCaml and Rust: picking the right tool for the job CUFP Joris GiovannangeliAhrefs Research | ||
10:55 - 11:20 Talk | Distributed load testing with MZBench CUFP |
10:30 - 10:50 Demonstration | Demo — African Polyphony and Polyrhythm FARM Chris FordThoughtWorks (UK) Ltd. Pre-print | ||
10:50 - 11:10 Demonstration | Demo — Vivid: Sound Synthesis with Haskell and SuperCollider FARM Pre-print | ||
11:10 - 11:40 Talk | GALE: A Functional Graphic Adventure Library and Engine FARM Ivan PerezUniversity of Nottingham, UK |
11:20 - 12:00 Coffee break | Saturday coffee break 2 Catering |
12:00 - 12:25 Talk | On Unsatisfiability HIW J. Garrett MorrisUniversity of Kansas, USA |
12:00 - 12:25 Talk | Gens N' Roses: Appetite for Reduction CUFP Jacob StanleyAmbiata |
12:00 - 12:30 Talk | Modelling the Way Mathematics Is Actually Done FARM |
12:25 - 14:00 Lunch | Saturday lunch Catering |
14:00 - 14:25 Talk | Why GHC Core and Linear Logic Should be Best Friends HIW | ||
14:25 - 14:50 Talk | Demand Analysis vs. Call Arity HIW Sebastian GrafKarlsruhe Institute of Technology | ||
14:50 - 15:00 Talk | Lightning Talk Slot #2 HIW |
14:00 - 14:25 Talk | Formally Verifying a Smart-Contract Language Implementation with Isabelle CUFP Simon MeierDigital Asset | ||
14:25 - 14:50 Talk | Haskell games and apps for iOS and Android CUFP Ivan PerezUniversity of Nottingham, UK |
14:00 - 15:00 Talk | FAUST Tutorial for Functional Programmers FARM |
14:50 - 15:30 Coffee break | Saturday coffee break 3 Catering |
15:30 - 15:55 Talk | IDE Support in GHC HIW | ||
15:55 - 16:20 Talk | Tracking GHC Performance HIW | ||
16:20 - 16:30 Talk | Lightning Talk Slot #3 HIW |
15:30 - 15:55 Talk | Using Haskell to run a datacenter CUFP | ||
15:55 - 16:20 Talk | Functional Facades over Legacy Code CUFP |
15:30 - 16:20: Session 5: DemosFARM at L3 Chair(s): David JaninBordeaux INP / CNRS LaBRI / Bordeaux University | |||
15:30 - 15:50 Demonstration | Demo — The Arpeggigon: A Functional Reactive Musical Automaton FARM Henrik NilssonUniversity of Nottingham, UK Pre-print | ||
15:50 - 16:10 Demonstration | Demo — Ait: A Concatenative Language for Creative Programming FARM Pre-print |
16:20 - 16:50 Coffee break | Saturday coffee break 4 Catering |
16:50 - 17:15 Talk | An Experiment in Fragment-Based Code Distribution HIW Philipp SchusterUniversity of Tübingen | ||
17:15 - 17:50 Talk | Lightning Talk Slot #4 HIW |
16:50 - 17:15 Talk | Building the largest payment sandbox on a tiny machine CUFP | ||
17:15 - 17:40 Talk | Using Functional Programming to Accelerate Translational Research at Pfizer CUFP Austin HuangPfizer |
16:50 - 17:40: Session 6: Papers/DemosFARM at L3 Chair(s): Henrik NilssonUniversity of Nottingham, UK | |||
16:50 - 17:20 Talk | Unified Media Programming: An Algebraic Approach FARM Simon ArchipoffCNRS LaBRI, Inria Bordeaux,, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University | ||
17:20 - 17:40 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 Social Event | FARM Evening Of Algorithmic Arts Social Events |
Sun 3 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sun 3 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Mon 4 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Mon 4 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Tue 5 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Tue 5 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 6 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Thu 7 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Thu 7 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Fri 8 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
Fri 8 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change
Room | 9:00 | 30 | 10:00 | 30 | 11:00 | 30 |
---|