Podcasts about icfp

Helen Burge, Deputy Chief Operations Officer, shares 6 tools to help SBLs have more strategic conversations with their Head & SLT… or as we like to call it, ‘The One With All The Tools'…  If you're a Friends fan, let's just say you're in for a real treat! The episode at a glance: [4:02] – Helen explains why SBLs need a toolkit for strategic conversations with the SLT [6:06] – Helen shares the first two tools for the first part of the strategic improvement cycle – the diagnostic phase [12:30] – Helen talks about ICFP as a strategic tool [17:22] – We move into the prioritisation phase where a vacuum cleaner takes centre stage… [22:46] – Helen and I get SMART as we talk about how this tool can be effective outside of performance management [27:22] – Helen explains how asking ‘why' can be useful when it comes to tackling someone who says ‘but we've always done it this way' [31:00] – We look at how the tools fit together and in what contexts they can be useful [34:28] – Helen tells us which of the 6 tools is her favourite and why Related content: - https://twitter.com/DeputyCOOatTPLT (Follow Helen on Twitter) - https://wafflesofansbl.com/ (Check out Helen's blog) If you're a School Business Leader… - https://www.ljbusinessofeducation.co.uk/sbl-surgery-4-how-to-be-seen-as-a-team-player/ (How To Be Seen As A Team Player) - https://www.ljbusinessofeducation.co.uk/risk-strategy/ (How To Implement A Risk Management Strategy) - https://www.gov.uk/guidance/integrated-curriculum-and-financial-planning-icfp (ICFP – Integrated Curriculum Financial Planning) Want to be a guest on the podcast? https://form.jotform.com/211131795465355 (Click here to leave me your details and I'll be in touch soon!) Subscribe: ·      If you haven't already, make sure you hit subscribe in your podcast player so you don't miss out on future episodes!  ·      https://school-business-leadership.captivate.fm/listen (Or click here if it's easier!) Get in touch: You know I love to hear from you so please pop me an email or get in touch on social media to let me know what you think of the show and what you'd like to see in the future! You can find Laura here… -       https://www.ljbusinessofeducation.co.uk/ (Website, Blog & Free Resources) -       https://twitter.com/lauraljbusiness/ (Twitter) -       https://www.instagram.com/lauraljbusiness/ (Instagram) -       https://www.facebook.com/lauraljbusiness/ (Facebook) -       https://www.linkedin.com/in/lauraljbusiness/ (LinkedIn)

Join us for a story based podcast where we go back in time to the late 90s when the financial planning profession was abuzz with the possibility of something great (and at times unthinkable) that was about to happen. - the merging of professional organizations to create one professional membership organization.

Join us for a story based podcast where we go back in time to the late 90s when the financial planning profession was abuzz with the possibility of something great (and at times unthinkable) that was about to happen.

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 tools that traffic in source code depend on these rules to present information to users and to soundly perform their operations. In this paper, we show how to lift scoping rules defined on a core language to rules on the surface, a process of scope inference. In the process we introduce a new representation of binding structure--scope as a preorder--and present a theoretical advance: proving that a desugaring system preserves alpha-equivalence even though scoping rules have been provided only for the core language. We have also implemented the system presented in this paper.

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, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks. A prototype implementation is available.

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 means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As evidence, we present the first complete proof of consistency for a language with closed type families.

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 likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.

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 services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.

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 applications do expose interfaces that are higher-order in spirit, the simplicity of the network protocols forces them to rely on brittle low-level encodings. To bridge the apparent semantic gap, programmers introduce ad-hoc and error-prone defensive code. Inspired by Design by Contract, we choose a different route to bridge this gap. We introduce Whip, a contract system for modern services. Whip (i) provides programmers with a higher-order contract language tailored to the needs of modern services; and (ii) monitors services at run time to detect services that do not live up to their advertised interfaces. Contract monitoring is local to a service. Services are treated as black boxes, allowing heterogeneous implementation languages without modification to services' code. Thus, Whip does not disturb the loosely coupled nature of modern services.

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 resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous pi-calculus into our language.

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 dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.

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 statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee--the so-called refined criteria, advocated by Siek et al. We develop System F-G, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F-C, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F-G and System F-C, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F-G satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

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, data type specifications, assertions, proofs, and programs, all in the same language. Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing natively implemented procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.

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 induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier 'forall' which lets us ignore sizes in terms for equality checking, alongside with a second quantifier 'Pi' for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type-shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.

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 two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler's core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results--chiefly, type safety, along with theorems that relate these two languages--have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell's term language does not correspond to a consistent logic.

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 ultimate abstraction-abstraction, a platform for quickly and easily building new ultimate abstractions. This pearl demonstrates Racket's power by taking a leisurely walk through the implementation of a DSL for Lindenmayer systems, the computational model par excellence of theoretical botany.

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 operations that we wish to perform on abstract syntax trees. We introduce "visitors", a simple type-directed facility for generating visitor classes that have no knowledge of binding. Separately, we present "alphaLib", a library of small hand-written visitor classes, each of which knows about a specific binding construct, a specific representation of names, and-or a specific operation on abstract syntax trees. By combining these components, a wide range of operations can be defined. Multiple representations of names can be supported, as well as conversions between representations. Binding structure can be described either in a programmatic style, by writing visitor methods, or in a declarative style, via preprogrammed binding combinators.

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, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages.

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 exported) top-level functions and places with cyclic (recursive) dependencies, after which FUSION can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented FUSION and evaluated it on the benchmarks from the LiquidHaskell suite totalling about 12KLOC. FUSION checks an existing safety benchmark suite using about half as many templates as previously required and nearly 2x faster. In a new set of theorem proving benchmarks FUSION is both 10 - 50x faster and, by synthesizing the most precise types, avoids false alarms to make verification possible.

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 strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to beta-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a beta-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.

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 application domain (e.g., compiler optimization validation) to queries that can be discharged with a highly optimized solver. But the correctness of the reductions themselves is rarely verified in practice, limiting the confidence that the solver's output establishes the desired domain-level property. This paper presents SpaceSearch, a new library for developing solver-aided tools within a proof assistant. A user builds their solver-aided tool in Coq against the SpaceSearch interface, and the user then verifies that the results provided by the interface are sufficient to establish the tool's desired high-level properties. Once verified, the tool can be extracted to an implementation in a solver-aided language (e.g., Rosette), where SpaceSearch provides an efficient instantiation of the SpaceSearch interface with calls to an underlying SMT solver. This combines the strong correctness guarantees of developing a tool in a proof assistant with the high performance of modern SMT solvers. This paper also introduces new optimizations for such verified solver-aided tools, including parallelization and incrementalization. We evaluate SpaceSearch by building and verifying two solver-aided tools. The first, SaltShaker, checks that RockSalt's x86 semantics for a given instruction agrees with STOKE's x86 semantics. SaltShaker identified 7 bugs in RockSalt and 1 bug in STOKE. After these systems were patched by their developers, SaltShaker verified the semantics' agreement on 15,255 instruction instantiations in under 2h. The second tool, BGProof, is a verified version of an existing Border Gateway Protocol (BGP) router configuration checker. Like the existing checker, BGProof scales to checking industrial configurations spanning over 240 KLOC, identifying 19 configuration inconsistencies with no false positives. However, the correctness of BGProof has been formally proven, and we found 2 bugs in the unverified implementation. These results demonstrate that SpaceSearch is a practical approach to developing efficient, verified solver-aided tools. We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed lambda-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.

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 result to reduce them away. We present a simple, linear-time algorithm for CPS conversion that introduces no administrative redexes. In fact, the output term is a normal form in a reduction system that generalizes the notion of 'administrative redexes' to what we call 'no-brainer redexes,' that is, redexes whose reduction shrinks the size of the term. We state the theorems which establish the algorithm's desireable properties, along with sketches of the full proofs.

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 computation rules derived from second-order algebraic theories. To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of second-order computation in non-trivial manner. In particular, our choice of Yokoyama's deterministic second-order patters as a syntactic construct of rules is important to cover a wide range of examples, such as Hasegawa's linear lmd-calculus. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and computational lmd-calculi, Staton's theory of reading and writing bits, Plotkin and Power's theory of states, and Stark's theory of pi-calculus.

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 that a high-level language can compete in this demanding space, but extracting reusable lessons from this success is difficult due to Ziria's lack of a formal semantics. Our first contribution is a core language, operational semantics, and type system for Ziria. The insight we gained through developing this operational semantics led to our second contribution, consisting of two program transformations. The first is fusion, which can eliminate intermediate queues in Ziria programs. Fusion subsumes many one-off optimizations performed by the original Ziria compiler. The second transformation is pipeline coalescing, which reduces execution overhead by batching IO. Pipeline coalescing relies critically on fusion and provides a much simpler story for the original Ziria compiler's "vectorization" transformation. These developments serve as the basis of our third contribution, a new compiler for Ziria that produces significantly faster code than the original compiler. The new compiler leverages our intermediate language to help eliminate unnecessary memory traffic. As well as providing a firm foundation for the Ziria language, our work on an operational semantics resulted in very real software engineering benefits. These benefits need not be limited to SDR--the core language and accompanying transformations we present are applicable to other domains that require processing streaming data at high speed.

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. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically known functions, and specialising calls to known functions with no free variables. Finally, we verify the translation to a lower-level IL that only supports closed, first-order functions. These compilation steps resemble those found in other compilers (especially OCaml). Our contribution here is the design of the semantics of the IL, and the demonstration that our verification techniques over this semantics work well in practice at this scale. The entire development was carried out in the HOL4 theorem prover.

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 about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialised notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures. We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed lambda-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.

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-Lavaud (Microsoft Research), Catalin Hritcu (India and Paris), Karthikeyan Bhargavan (Inria, France), Cedric Fount (Microsoft Research), Nikhil Swamy (Microsoft Research, United States). We present Low, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low is a shallow embedding of a small, sequential, well-behaved subset of C in F, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model a la CompCert, and it provides the control required for writing efficient low-level security-critical code. By virtue of typing, any Low program is memory safe. In addition, the programmer can make full use of the verification power of F to write high-level specifications and verify the functional correctness of Low code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.

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 lookup and updates, good cache utilization, but also logarithmic concatenation and slicing. Our goal is to bring the benefits of persistent data structures to the discipline of systems programming via generic yet efficient immutable vectors supporting transient batch updates. We describe a C++ implementation that can be integrated in the runtime of higher level languages with a C core (Lisps like Guile or Racket, but also Python or Ruby), thus widening the access to these persistent data structures.

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 verify an autonomous system like a self-driving car? This talk will attempt to lay out the problem space, and offer some ideas for how the verification community might start tackling the problem of assuring AI.

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 the type checker. As a refinement Pałka et al. propose to generate programs in a goal-directed, bottom-up reading up of the typing relation. We have written such a generator. However many of the generated programs has output that depend on the evaluation order, which is commonly under-specified in languages such as OCaml, Scheme, C, C++, etc. In this paper we develop a type and effect system for conservatively detecting evaluation-order dependence and propose its goal-directed reading as a generator of programs that are independent of evaluation order. We illustrate the approach by generating programs to test OCaml's two compiler backends against each other and report on a number of bugs we have found doing so.

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 partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.

Daniel Winograd-Cort University of Pennsylvania, USA, gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Andreas Haeberlen and Aaron Roth, University of Pennsylvania, USA. Differential privacy is a widely studied theory for analyzing sensitive data with a strong privacy guarantee--any change in an individual's data can have only a small statistical effect on the result--and a growing number of programming languages now support differentially private data analysis. A common shortcoming of these languages is poor support for adaptivity. In practice, a data analyst rarely wants to run just one function over a sensitive database, nor even a predetermined sequence of functions with fixed privacy parameters; rather, she wants to engage in an interaction where, at each step, both the choice of the next function and its privacy parameters are informed by the results of prior functions. Existing languages support this scenario using a simple composition theorem, which often gives rather loose bounds on the actual privacy cost of composite functions, substantially reducing how much computation can be performed within a given privacy budget. The theory of differential privacy includes other theorems with much better bounds, but these have not yet been incorporated into programming languages. We propose a novel framework for adaptive composition that is elegant, practical, and implementable. It consists of a reformulation based on typed functional programming of the privacy filters of Rogers et al (2016), together with a concrete realization of this framework in the design and implementation of a new language, called Adaptive Fuzz. Adaptive Fuzz transplants the core static type system of Fuzz to the adaptive setting by wrapping the Fuzz typechecker and runtime system in an outer adaptive layer, allowing Fuzz programs to be conveniently constructed and type-checked on the fly. We describe an interpreter for Adaptive Fuzz and report results from two case studies demonstrating its effectiveness for implementing common statistical algorithms over real data sets.

Praveen Narayanan, Indiana University, USA, gives the third presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Chung-Chief Shan, Indiana University, USA. Probabilistic programming systems make machine learning methods modular by automating inference. Recent work by Shan and Ramsey (2017) makes inference itself modular by automating the common component of conditioning. Their work introduces a symbolic program transformation that treats conditioning generally via the measure-theoretic notion of disintegration. This technique, however, is limited to conditioning a single scalar variable. As a step towards tackling realistic machine learning applications, we have extended the disintegration algorithm to symbolically condition arrays in probabilistic programs. The extended algorithm implements lifted disintegration, where repetition is treated symbolically and without unrolling loops. The technique uses a language of index variables for tracking expressions at various array levels. We find that the method works well for arbitrarily-sized arrays of independent random choices, with the conditioning step taking time linear in the number of indices needed to select an element.

David Darais, University of Maryland, USA, gives the first presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Nicholas Labich, David Van Horn, Phuc C. Nguyen, University of Maryland, USA. In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a nice basis for a wide variety of collecting semantics, abstract interpretations, symbolic executions, and their intermixings. But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called 'pushdown control flow' property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language. The first approaches to achieve this property for higher-order languages appeared within the last ten years, and have since been the subject of many papers. These approaches start from a state-machine semantics and uniformly involve significant technical engineering to recover the precision of pushdown control flow. In contrast, starting from a definitional interpreter, the pushdown control flow property is inherent in the meta-language and requires no further technical mechanism to achieve.

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 comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features. We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.

Louis Mandel (IBM) gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Joshua Auerbach, Martin Hirzel, Avraham Shinnar, Jerome Simeon, IBM Research, USA. Designing and prototyping new features is important in many industrial projects. Functional programming and formal verification tools can prove valuable for that purpose, but lead to challenges when integrating with existing product code or when planning technology transfer. This article reports on our experience using the Coq proof assistant as a prototyping environment for building a query compiler intended for use in IBM's ODM Insights product. We discuss the pros and cons of using Coq for this purpose and describe our methodology for porting the compiler to Java, as required for product integration.

William E. Byrd, University of Utah, USA, gives the fourth presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Co-written by Gregory Rosenblatt, Matthew Might, Michael Ballantyne (University of Utah). We present seven programming challenges in Racket, and an elegant, unified approach to solving them using constraint logic programming in mini Kanren.

Conal Elliott, Target, USA United States, gives the third presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Parallel programming, whether imperative or functional, has long focused on arrays as the central data type. Meanwhile, typed functional programming has explored a variety of data types, including lists and various forms of trees. Generic functional programming decomposes these data types into a small set of fundamental building blocks: sum, product, composition, and their associated identities. Definitions over these few fundamental type constructions then automatically assemble into algorithms for an infinite set of data types--some familiar and some new. This paper presents generic functional formulations for two important and well-known classes of parallel algorithms: parallel scan (generalized prefix sum) and Fast Fourier Transform (FFT). Notably, arrays play no role in these formulations. Consequent benefits include a simpler and more compositional style, much use of common algebraic patterns--such as Functor, Applicative, Foldable, and Traversable--and freedom from possibility of run-time indexing errors. The functional generic style also clearly reveals deep commonality among what otherwise appears to be quite different algorithms. Instantiating the generic formulations to "top-down" and "bottom-up" trees as well as "bushes", two well-known algorithms for each of parallel scan and FFT naturally emerge, as well as two possibly new algorithms.

Jean-Philippe Bernardy, University of Gothenburg, gives the second presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. This paper proposes a new specification of pretty printing which is stronger than the state of the art: we require the output to be the shortest possible, and we also offer the ability to align sub-documents at will. We argue that our specification precludes a greedy implementation. Yet, we provide an implementation which behaves linearly in the size of the output. The derivation of the implementation demonstrates functional programming methodology.

Mike Spivey, University of Oxford, UK, gives the first presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Coroutine pipelines provide an attractive structuring mechanism for complex programs that process streams of data, with the advantage over lazy streams that both ends of a pipeline may interact with the I-O system, as may processes in the middle. Two popular Haskell libraries, Pipes and Conduit, support such pipelines. In both libraries, pipelines are implemented in a direct style by combining a free monad of communication events with an interpreter for (pseudo-)parallel composition that interleaves the events of its argument processes. These implementations both suffer from a slow-down when processes are deeply nested in sequence or in parallel. We propose an alternative implementation of pipelines based on continuations that does not suffer from this slow-down. What is more, the implementation is significantly faster on small, communication-intensive examples even where they do not suffer from the slow-down, and faster even than comparable programs based on lazy streams. The continuation-based implementation may be derived from the direct-style implementation by algebraic reasoning.

Roberto Di Cosmo (Inria, France and University of Paris Diderot, France), gives the fourth presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Benjamin Canou (OCamlPro) and Gregoire Henry (OCamlPro). This article describes the key innovations used in the massive open online course 'Introduction to Functional Programming using OCaml that has run since the fall semester of 2015. A fully in-browser development environment with an integrated grader provides an exceptional level of feedback to the learners. A functional library of grading combinators greatly simplifies the notoriously complex task of writing test suites for the exercises, and provides static type-safety guarantees on the tested user code. Even the error-prone manual process of importing the course content in the learning platform has been replaced by a functional program that describes the course and statically checks its contents. A detailed statistical analysis of the data collected during and after the course assesses the effectiveness of these innovations.

Joachim Breiner, University of Pennsylvania, United States, gives the third presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Chris Smith Google, USA. Implementing multi-player networked games by broadcasting the player's input and letting each client calculate the game state -- a scheme known as lock-step simulation -- is an established technique. However, ensuring that every client in this scheme obtains a consistent state is infamously hard and in general requires great discipline from the game programmer. The thesis of this pearl is that in the realm of functional programming -- in particular with Haskell's purity and static pointers -- this hard problem becomes almost trivially easy. We support this thesis by implementing lock-step simulation under very adverse conditions. We extended the educational programming environment CodeWorld, which is used to teach math and programming to middle school students, with the ability to create and run interactive, networked multi-user games. Despite providing a very abstract and high-level interface, and without requiring any discipline from the programmer, we can provide consistent lock-step simulation with client prediction.

Ivan Perez, University of Nottingham, UK, gives the second presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Henrik Nilsson, University of Nottingham, UK. Many types of interactive applications, including video games, raise particular challenges when it comes to testing and debugging. Reasons include de-facto lack of reproducibility and difficulties of automatically generating suitable test data. This paper demonstrates that certain variants of Functional Reactive Programming (FRP) implemented in pure functional languages can mitigate such difficulties by offering referential transparency at the level of whole programs. This opens up for a multi-pronged approach for assisting with testing and debugging that works across platforms, including assertions based on temporal logic, recording and replaying of runs (also from deployed code), and automated random testing using QuickCheck. The approach has been validated on real, non-trivial games implemented in the FRP system Yampa through a tool providing a convenient Graphical User Interface that allows the execution of the code under scrutiny to be controlled, moving along the execution time line, and pin-pointing of violations of assertions on PCs as well as mobile platforms.

Leif Andersen (Northeastern University, USA) gives the first presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Stephen Chang (Northeastern University, USA) and Matthias Felleisen (Northeastern University, USA). The Racket doctrine tells developers to narrow the gap between the terminology of a problem domain and general programming constructs by creating languages instead of just plain programs. This pearl illustrates this point with the creation of a relatively simple domain-specific language for editing videos. To produce the video proceedings of a conference, for example, video professionals traditionally use 'non-linear' GUI editors to manually edit each talk, despite the repetitive nature of the process. As it turns out, video editing naturally splits the work into a declarative phase and an imperative rendering phase at the end. Hence it is natural to create a functional-declarative language for the first phase, which reduces a lot of manual labor. This user-facing DSL utilizes a second, internal DSL to implement the second phase, which is an interface to a general, low-level C library. Finally, we inject type checking into our language via another DSL that supports programming in the language of type formalisms. In short, the development of the video editing language cleanly demonstrates how the Racket doctrine naturally leads to the creation of language hierarchies, analogous to the hierarchies of modules found in conventional functional languages.

Chris Martens (North Carolina State University, United States) gives the first talk in the ICFP conference. Generativity is an increasingly popular and useful concept, referring to a machine's ability to respond to user input with new constructions not foreseen by the programmer. Yet increasingly, people treat computational systems as unknowable black-box systems, writing off the possibility of forming mental models that allow a collaborative relationship between human insight and fast computation. Test phrase here. I argue for the efficacy of transparent, compositional semantics for collaborating with virtual agents and deriving insights from system models. Having built systems based on automated reasoning for linear logic and epistemic modal logic, we can formalize notions of belief, intention, and action, in order to create virtual agents that behave in ways that humans can reason about based on intuitions about goal-driven behavior. For example, some of Grice's maxims of conversation can be seen as derivable consequences of these principles. Ongoing work includes applying these formalisms to the tasks of navigating unknown rule systems in virtual environments, social skills training, and generative storytelling.

Hernan Melgratti (University of Buenos Aires, Argentina), gives the first talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written by Luca Padovani (University of Turin, Italy). Contracts have proved to be an effective mechanism that helps developers in identifying those modules of a program that violate the contracts of the functions and objects they use. In recent years, sessions have established as a key mechanism for realizing inter-module communications in concurrent programs. Just like values flow into or out of a function or object, messages are sent on, and received from, a session endpoint. Unlike conventional functions and objects, however, the kind, direction, and properties of messages exchanged in a session may vary over time, as the session progresses. This feature of sessions calls for contracts that evolve along with the session they describe. In this work, we extend to sessions the notion of chaperone contract (roughly, a contract that applies to a mutable object) and investigate the ramifications of contract monitoring in a higher-order language that features sessions. We give a characterization of correct module, one that honors the contracts of the sessions it uses, and prove a blame theorem. Guided by the calculus, we describe a lightweight implementation of monitored sessions as an OCaml module with which programmers can benefit from static session type checking and dynamic contract monitoring using an off-the-shelf version of OCaml.

This episode is presented in English! Fredrik speaks to Alejandro Russo about information security. Using Haskell, it is possible to create a library which can guarantee information security even when information (say, your password to a library checking password strength) is passed on to third-party code. We discuss Alejandro’s paper on this topic and the much wider applicability and possibilities of the ideas - they’re hopefully making their way into browsers! We also talk a bit about how to inform yourself about security (and what not to do), as well as discuss the flow of knowledge between academia and non-academia. Alejandro Russo is an associate professor at Chalmers University of Technology working on the intersection of functional languages, security, and systems. He is the recipient of a Google Research Awards and several grants from the Swedish research agencies Vetenskapsrådet, STINT, and Barbro Osher foundation. Internationally, Prof. Russo worked on prestigious research institutions like Stanford University, where he was appointed visiting associate professor. His research ranges from foundational aspects of security to developing tools tosecure software written in Haskell, Python, and JavaScript. Links   Alejandro Russo Functional programming BBS Modem Two Can Keep a Secret, If One of Them Uses Haskell - Alejandro’s paper ICFP 2015 Functional pearls Haskell Access control Information-flow control Side-effects Haskell 98 Dependent-type languages JSFlow - IFC for Javascript, created by people at Chalmers People at Chalmers and Cornell creating Java compilers GDPR - EU directive to strengthen data protection for individuals Webassembly Gradual typing Buffer overflow Dangling pointers Fuzz testing IEEE security and privacy conferences ACMCCS OSDI SOSP Pony Rust Data race Linear types Affine types There is code written in Rust inside Firefox since August 2016 COWL - Confinement with origin web labels Drop Alejandro a line! Under utveckling is a podcast by and for developers, created in sunny (cough) Gothenburg by us at TimeEdit. We would love your feedback on the topics we discuss! We are on Twitter as @uupodden and at Facebook as Under utveckling. If you enjoy the podcast we’d love a rating and review in iTunes!

On this weeks show we answered the question how does one make good financial decisions in a world dominated by risk and uncertainty. We discussed the book The Power of Choice which is dedicated to the idea that each of us has a choice to better our lives, empower ourselves and reach our goals.  We were joined by author Jeff Kanaly. Jeff is Vice Chairman of Kanaly Trust and serves on the organization's board of directors. He has been with the company for over 35 years and concentrates on corporate strategic planning. An important focus for Jeff is ensuring that the high quality of service Kanaly Trust was founded on continues to be the central focus of the organization. He specializes in serving multi-generational families due to his depth of experience in high level, intricate estate and financial planning practices. A graduate of the University of Texas at Austin, Jeff holds a Bachelor of Business Administration degree in Finance. He is a CERTIFIED FINANCIAL PLANNERTM practitioner and a Certified Trust and Financial Advisor (CTFA). He is a member of the Financial Planning Association (FPA), the Houston Chapter of the FPA, the Houston Estate and Financial Forum (HEFF), and the Association of Trust Organizations (ATO). Jeff has served on many public and professional committees. He is a past national board member of the Financial Planning Association (FPA) and previously served on its Tax Sub-committee. He was involved in the merger of the Institute of Certified Financial Planners (ICFP) and the International Association of Financial Planners (IAFP) that formed the FPA. He was responsible for the coordination of the FPA's Pro-bono Program, has served on the ICFP board and on its Practice Management Committee. He is past president of the Association of Independent Trust Companies (AITCO now ATO), and previously served on its board of directors as treasurer. He is also a past chairman and president of the Houston Society ICFP.  Jeff also serves on the Investment Committee at Kanaly Trust.  Jeff has served on the board of directors of the American Heart Association in Northwest Harris County and on the board of Applause Theatre.  He is actively involved with the National MS Society, South Central Chapter as Chair of the Houston Leadership Council and was instrumental in launching the MS Entrepreneurs Program which helps those affected by MS at a grass-roots level.  In addition, Jeff was recently selected as the Investment Committee liaison for the South Central Region of the MS Society. Jeff's comments have appeared in such publications as Robb Report Worth, the Houston Business Journal and Financial Planning. To find out more click below the:   The Power Of Choice   Choice of A Lifetime   Kanaly Trust     You can listen live by going to www.kpft.org and clicking on the HD3 tab. You can also listen to this episode and others by podcast at:http://directory.libsyn.com/shows/view/id/moneymatters