MikiBeta : A General GUI Library for Visualizing Proof Trees

DOI10.1007/978-3-642-20551-4_6MaRDI QIDQ3003488zbMATH OpenOpenAlexFDO

Authors Kanako Sakurai, Kenichi Asai

Publication date 27 May 2011

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-20551-4_6

zbMATH Keywords

\(\lambda\)-calculusgraphical user interface (GUI)LablTkOCamlproof treeshift and resetSystem Ftwo-level typetype system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Recommendations

• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• ProofViz: an interactive visual proof explorer
• VMEXT: a visualization tool for mathematical expression trees
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• A generic graphic framework for combining inference tools and editing proofs and formulae
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Hiproofs: a hierarchical notion of proof tree
• Panoptes: an exploration tool for formal proofs

Cites work

• Generic programming with fixed points for mutually recursive datatypes
• scientific article; zbMATH DE number 1948185 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Semantics engineering with PLT Redex
• Two-level types and parameterized modules
• Types and programing languages

Describes a project that uses

Uses Software

• Coq
• OCaml
• MikiBeta
• PLT Redex

This page was built for publication: MikiBeta : A General GUI Library for Visualizing Proof Trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003488)