Justin Pombrio (Brown University, USA) gives the third talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. Co-written by Shriram Krishnamurthi (Brown University, USA) and Mitchell Wand (Northeastern University, USA). Many languages use syntactic sugar to define parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules, are not immediately evident. Nevertheless, IDEs, refactorers, and other t...
Jan 23, 2018•17 min•Transcript available on Metacast Martin Avanzini (University of Innsbruck, Austria) gives the second talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and constraint solving. Noticeably, the presented methodology can be fully automated...
Jan 23, 2018•19 min•Transcript available on Metacast Richard A. Eisenberg (Bryn Mawr College, USA) gives the first talk in the fifth panel, Inference and Analysis, on the 3rd day of the ICFP conference. Co-written by J. Garrett Morris (University of Kansas, USA). We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular mean...
Jan 23, 2018•16 min•Transcript available on Metacast Victor Lanvin (ENS Cachan, France) gives the third talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Giuseppe Castagna (CNRS, University of Paris Diderot). We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewi...
Jan 23, 2018•18 min•Transcript available on Metacast Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Taro Sekiyama (IBM Research, Japan), Atsushi Igarashi (Kyoto University, Japan). We study an extension of gradual typing--a method to integrate dynamic typing and static typing smoothly in a single language--to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both ...
Jan 22, 2018•18 hr 4 min•Transcript available on Metacast Amal Ahmed (Northeastern University, USA) gives the first talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Dustin Jamner (Northeastern University, USA), Jeremy G. Siek (Indiana University, USA), Philip Wadler (University of Edinburgh, UK). The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamica...
Jan 22, 2018•21 min•Transcript available on Metacast Peter Thiemann (University of Freiburg, Germany) gives the fourth talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written by Atsushi Igarashi (Kyoto University, Japan), Vasco Vasconcelos (University of Lisbon, Portugal), Philip Wadler (University of Edinburgh, UK). Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro s...
Jan 22, 2018•21 min•Transcript available on Metacast Stephanie Balzer (Carnegie Mellon University, USA) gives the third talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written Frank Pfenning (Carnegie Mellon University, USA). Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared res...
Jan 22, 2018•21 min•Transcript available on Metacast Lucas Waye (Harvard University, USA), gives the second talk in the third panel, Contracts and Sessions , on the 3rd day of the ICFP conference. Co-written by Christos Dimoulas (Harvard University, USA), Stephen Chong (Harvard University, USA). Modern service-oriented applications forgo semantically rich protocols and middleware when composing services. Instead, they embrace the loosely-coupled development and deployment of services that communicate via simple network protocols. Even though these...
Jan 22, 2018•18 min•Transcript available on Metacast Sebastian Ullrich (KIT, Germany), gives the fourth talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Gabriel Exner (Vienna University of Technology, Austria), Jared Roesch (University of Washington, USA), Jeremy Avigad (Carnegie Mellon University, USA), Leonardo De Moura (Microsoft Research). Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects,...
Jan 17, 2018•17 min•Transcript available on Metacast Andreas Abel (University of Gothenburg, Sweden), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Andrea Vezzosi (Chalmers University of Technology, Sweden), Theo Winterhalter (ENS Paris-Saclay, France). Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by inducti...
Jan 17, 2018•20 min•Transcript available on Metacast Antoine Vizard (University of Pennsylvania, USA), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Stephanie Weiricc (University of Pennsylvania, USA), Pedro Henrique Azevedo de Amorim (Ecole Polytechnique, University of Campinas, Brazil), Richard A. Eisenberg( Bryn Mawr College, USA). We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of...
Jan 17, 2018•19 min•Transcript available on Metacast Robby Findler (Northwestern University, USA), gives the first talk in the first panel, Domain-Specific Languages, on the 3rd day of the ICFP conference. Co-written by Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Northwestern University. Domain-specific languages are the ultimate abstraction, dixit Paul Hudak. But what abstraction should we use to build such ultimate abstractions? What is sauce for the goose is sauce for the gander: a language, of course! Racket is the ulti...
Jan 17, 2018•20 min•Transcript available on Metacast Francois Pottier (Inria, France), gives the second talk in the fourth panel, Program Construction, on the 2nd day of the ICFP conference. Traversing and transforming abstract syntax trees that involve name binding is notoriously difficult to do in a correct, concise, modular, customisable manner. We address this problem in the setting of OCaml, a functional programming language equipped with powerful object-oriented features. We use visitor classes as partial, composable descriptions of the oper...
Jan 17, 2018•18 min•Transcript available on Metacast Conal Elliott, Target, USA, gives the first talk in the fourth panel, Program Construction, on the 2nd day of the ICFP conference. It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, s...
Jan 16, 2018•18 min•Transcript available on Metacast Benjamin Cosman, University of California at San Diego, USA, gives the third talk in the second panel, Tools for Verification, on the 2nd day of the ICFP conference. Co-written by Ranjit Jhala, University of California at San Diego, USA. We introduce the FUSION algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is concise as the programmer need only write signatures for (externally e...
Jan 16, 2018•14 min•Transcript available on Metacast Konstantin Weitz (University of Washington, USA) gives the second talk in the second panel, Tools for Verification, on the 2nd day of the ICFP conference. Co-written by Steven Lyubomirsky, University of Washington, USA, Stefan Heule, Stanford University, USA, Emina Torlak, University of Washington, USA, Michael D. Ernst, University of Washington, USA, Zachary Matlock, University of Washington, USA. Many verification tools build on automated solvers. These tools reduce problems in a specific appl...
Jan 15, 2018•18 min•Transcript available on Metacast Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Co-written by Joonwon Choi, Benjamin Sherman, Adam Chlipala, Arvind (Massachusetts Institute of Technology, USA). It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning for har...
Jan 15, 2018•20 min•Transcript available on Metacast Milo Davis (Northeastern University, USA) gives the fourth talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP. Co-written by William Meehan and Olin Shivers (Northeastern University, USA). Algorithms that convert direct-style lambda-calculus terms to their equivalent terms in continuation-passing style (CPS) typically introduce so-called 'administrative redexes' -- useless artifacts of the conversion that must be cleaned up by a subsequent pass over the...
Jan 15, 2018•14 min•Transcript available on Metacast Thibaut Balabonski (LRI, France and University of Paris-Sud, France) gives the third talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. Co-written by Pablo Barenbaum (University of Buenos Aires, Argentina/IRIF, France/University of Paris Diderot, France), Eduardo Bonelli (CONICET, Argentina/Universidad Nacional de Quilmes, Argentina), Delia Kesner (IRIF/University of Paris Diderot, France). We present a call-by-need strategy for computing st...
Jan 15, 2018•19 min•Transcript available on Metacast Makoto Hamana (Gunma University, Japan), gives the first talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. We present a general methodology of proving decidability of equational theory of programming language concepts in the framework of second-order algebraic theories of Fiore, Hur and Mahmoud. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computati...
Dec 18, 2017•17 min•Transcript available on Metacast Geoffrey Mainland (Drexel University, USA) gives the fourth talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Software-defined radio (SDR) promises to bring the flexibility and rapid iterative workflow of software to radio protocol design. Many factors make achieving this promise challenging, not least of which are the high data rates and timing requirements of real-world radio protocols. The Ziria language and accompanying compiler demonstrated t...
Dec 18, 2017•18 min•Transcript available on Metacast Scott Owens University of Kent, UK, gives the third talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Co-written Michael Norrish, Ramana Kumar (Data61 at CSIRO, Australia and UNSW, Australia), Magnus O. Myreen (Chalmers University of Technology, Sweden), Yong Kiam Tan (Carnegie Mellon University, USA). We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Ve...
Dec 18, 2017•20 min•Transcript available on Metacast Alejandro Aguirre, IMDEA Software Institute, Spain, gives the second talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. Co-written by Gilles Berthe (IMDEA Software Institute, Spain), Marco Gaboardi (University at Buffalo, SUNY, USA), Deepak Garg (MPI-SWS, Germany), Pierre-Yves Strub (Ecole Polytechnique, France) Relational program verification is a variant of program verification where one can reason about two programs and as a special case ...
Dec 18, 2017•17 min•Transcript available on Metacast Jonathan Protzen, Microsoft Research, United States, gives the second talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Co-written by Jonathan Protzen (Microsoft Research, United States), Jean-Karim Zinzindohoué (Inria, France), Aseem Rastogi (Microsoft Research, India), Tahina Ramananandro (Microsoft Research, United States), Peng Wang (Massachusetts Institute of Technology, USA), Santiago Zanella-Beguelin (Microsoft Research), Antoine Delignat-L...
Dec 18, 2017•18 min•Transcript available on Metacast Juan Pedro Bolívar Puente, Independent Consultant, Sinusoidal Engineering, Germany, gives the first talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Relaxed Radix Balanced Trees (RRB-Trees) is one of the latest members in a family of persistent tree based data-structures that combine wide branching factors with simple and relatively flat structures. Like the battle-tested immutable sequences of Clojure and Scala, they have ffectively constant loo...
Dec 18, 2017•19 min•Transcript available on Metacast John Launchbury, Chief Scientist of Galois Inc, gives the second keynote of the ICFP conference. Somewhat ironically, just as traditional systems software finally comes within reach of detailed mathematical verification, the demand for verification technology is rapidly expanding into domains that pose very different kinds of challenges. How could a face recognition technology be verified, for example, when it is not clear even how to state a correctness property? Or how should we attempt to ver...
Dec 18, 2017•53 min•Transcript available on Metacast Jan Midtgaard, gives the fourth presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson, DTU, Denmark. How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typed by t...
Dec 18, 2017•18 min•Transcript available on Metacast Jan Stolarek, University of Edinburgh, UK, gives the third presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Wilmer Ricciotti, Roly Perera and James Cheney, and University of Edinburgh, UK. Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work, where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of part...
Dec 18, 2017•18 min•Transcript available on Metacast Ohad Kammar, University of Oxford, UK, gives the second presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Yannick Forster (Saarland University, Germany and University of Cambridge, UK), Sam Lindley (University of Edinburgh). We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comp...
Dec 13, 2017•18 min•Transcript available on Metacast 
