Скачать или смотреть William J . Bowman - Cur: Designing a less devious proof assistant

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur (https://github.com/wilbowma/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.

Slides with notes and demo code are available https://williamjbowman.com/#epa-less-...)