MikiBeta : A General GUI Library for Visualizing Proof Trees

DOI10.1007/978-3-642-20551-4_6zbMath1326.68072OpenAlexW35890323MaRDI QIDQ3003488

Kenichi Asai, Kanako Sakurai

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\)-calculustype systemproof treeSystem Fgraphical user interface (GUI)shift and resetLablTkOCamltwo-level type

Mathematics Subject Classification ID

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

Uses Software

• Coq
• OCaml
• MikiBeta
• PLT Redex

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Generic programming with fixed points for mutually recursive datatypes
• Two-level types and parameterized modules

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