Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
From MaRDI portal
Publication:5195279
DOI10.6092/ISSN.1972-5787/6298zbMath1451.68324arXiv1610.05593OpenAlexW2536147106MaRDI QIDQ5195279
Yu-Hui Lin, Rob Arthan, Gudmund Grov
Publication date: 18 September 2019
Full work available at URL: https://arxiv.org/abs/1610.05593
Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- A higher-order implementation of rewriting
- Edinburgh LCF. A mechanized logic of computation
- Fundamentals of algebraic graph transformation
- A Graphical Language for Proof Strategies
- Polar: A Framework for Proof Refactoring
- HOL Light: An Overview
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- A Brief Overview of HOL4
- The Four Colour Theorem: Engineering of a Formal Proof
- The Zipper
- Open-graphs and monoidal theories
- Refactoring Proofs with Tactician
- Now f is continuous (exercise
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- Towards Formal Proof Script Refactoring
- Jape: A calculator for animating proof-on-paper
- Theorem Proving in Higher Order Logics
- Interactive Simplifier Tracing and Debugging in Isabelle
This page was built for publication: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
