Mathematics and Computation

A blog about mathematics for computers

Postsby categoryby yearall

Posts in the category Every proof assistant

We shall finish the semester with a "Every proof assistant" talk by William Bowman. Note that we start an hour later than usual, at 17:00 UTC+2.

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur

Abstract:

Dijkstra said that our tools can have a profound and devious influence on our thinking. I find this especially true of modern proof assistants, with "devious" out-weighing "profound". Cur is an experiment in design that aims to be less devious. The design emphasizes language extension, syntax manipulation, and DSL construction and integration. This enables the user to be in charge of how they think, rather than requiring the user to contort their thinking to that of the proof assistant. In this talk, my goal is to convince you that you want similar capabilities in a proof assistant, and explain and demonstrate Cur's attempt at solving the problem.

The talk video recording and slides with notes and demo code are available.

Upcoming talks: Anders Mörtberg's talk on Cubical Agda will take place in September 2020.

continue reading

This week shall witness a performance by Conor McBride.

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2

Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted several times in the late 2000s and never even reached cruising altitude. This talk is absolutely not an attempt to persuade you to start using it. Rather, it is an exploration of the ideas which drove it: proof irrelevant observational equality, first class datatype descriptions, nontrivial equational theories for neutral terms. We may yet live to see such things. Although the programming language elaborator never happened, the underlying proof engine was accessible via an imperative interface called "Cochon": we did manage some interesting constructions, at least one of which I can walk through. I'll also explore the reasons, human and technological, why the thing did not survive the long dark.

The video recording of the talk.

Upcoming talks:

continue reading

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring computational versions of function extensionality, higher inductive types, and univalence. Building on ideas from Epigram, Agda, and Idris, redtt introduces a new cubical take on interactive proof development with holes. We will first introduce the basics of cubical type theory and then dive into an interactive demonstration of redtt’s features and its mathematical library.

After this we will catch a first public glimpse of the future of redtt, a new prototype that our team is building currently code-named “cooltt”: cooltt introduces syntax to split on disjunctions of cofibrations in arbitrary positions, implementing the full definitional eta law for disjunction. While cooltt is still in the early stages, it already has full support for univalence and cubical interactive proof development.

The video recording of the talk.

Upcoming talks:

continue reading

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions.

Our experience demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.

The video recording of the talk.

Upcoming talks:

continue reading

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapidly prototyping of new language features.

Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration.

This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems.

The video recording of the talk.

The spring schedule of talks is planned as follows:

continue reading (1 comment)

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

continue reading (10 comments)
Postsby categoryby yearall