Is it true? Why questions about the news are changing

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.

Creative Commons Licence

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series

International Conference on Functional Programming 2017

People

Keywords

Department: Department of Computer Science

Date Added: 17/01/2018

Duration: 00:16:35

Download

Normalization by Evaluation for Sized Dependent Types

Series

International Conference on Functional Programming 2017

Embed

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.

Creative Commons Licence

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series

International Conference on Functional Programming 2017

People

Keywords

Department: Department of Computer Science

Date Added: 17/01/2018

Duration: 00:20:21

Download

A Specification for Dependent Types in Haskell

Series

International Conference on Functional Programming 2017

Embed

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.

Creative Commons Licence

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series

International Conference on Functional Programming 2017

People

Keywords

Department: Department of Computer Science

Date Added: 17/01/2018

Duration: 00:18:51

Download

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)

Series

International Conference on Functional Programming 2017

Embed

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.

Creative Commons Licence

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series

International Conference on Functional Programming 2017

People

Keywords

Department: Department of Computer Science

Date Added: 17/01/2018

Duration: 00:20:08

Download

Visitors Unchained

Series

International Conference on Functional Programming 2017

Embed

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.

Creative Commons Licence

Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK (BY-NC-SA): England & Wales; https://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series

International Conference on Functional Programming 2017

People

Keywords

Department: Department of Computer Science

Date Added: 17/01/2018

Duration: 00:17:59

Download

Teach us how we may pray

Series

Designing English: Graphics on the medieval page

Embed

AElfric of Eynsham teaches the congregation to recite the Lord’s Prayer in English, 'Thu ure faeder'. MS. Hatton 115, fol. 10r. Composed 990-995, copied in the second half of the 1000s. Read by Andy Orchard.

Episode Information

Series

Designing English: Graphics on the medieval page

People

Keywords

Department: Bodleian Libraries

Date Added: 16/01/2018

Duration: 00:01:16

Download

Come and dance with me in Ireland

Series

Designing English: Graphics on the medieval page

Embed

The lyrics of dance songs about love and longing, jotted down without music. MS. Rawl. D. 913, fol. 1r-v. Copied in the early 1300s. Read by Helen Appleton, Daniel Wakelin.

Episode Information

Series

Designing English: Graphics on the medieval page

People

Keywords

Department: Bodleian Libraries

Date Added: 16/01/2018

Duration: 00:01:04

Download

If it be played

Series

Designing English: Graphics on the medieval page

Embed

In the play The Burial of Christ, Joseph, Mary Magdalen and three other women cry out when they see Jesus on the Cross. MS. e Musaeo 160, fol. 141r. Copied c. 1518–1520. Read by Helen Appleton, Angela O'Brien, Daniel Sawyer, Wing Tan Lai.

Episode Information

Series

Designing English: Graphics on the medieval page

People

Keywords

Department: Bodleian Libraries

Date Added: 16/01/2018

Duration: 00:01:31

Download

First entereth Wisdom

Series

Designing English: Graphics on the medieval page

Embed

In the play Wisdom, the devil tempts three godly people into sins – lust and other ‘French fashions’. MS. Digby 133, fol. 158r. Copied in the late 1400s. Read by Arka Chakraborty, Matthew Day, Ben Sims, Daniel Sawyer.