Sakurai, Kanako; Asai, Kenichi MikiBeta: a general GUI library for visualizing proof trees. System description and demonstration. (English) Zbl 1326.68072 Alpuente, María (ed.), Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-20550-7/pbk). Lecture Notes in Computer Science 6564, 84-98 (2011). Summary: This paper describes and demonstrates MikiBeta, a general graphical user interface (GUI) library we are developing for visualizing proof trees. Using MikiBeta, one can construct a proof tree step by step by selecting a judgement and clicking an inference rule to apply, without worrying about instanciating metavariables with their contents, copying similar expressions for each judgement, or how much space is necessary to visualize the complete proof tree. To cope with different kinds of proof trees, MikiBeta is parameterized with user-defined judgements and inference rules. Because MikiBeta allows arbitrary side-effect-free user code in inference rules, one can construct GUIs with complex operations such as environment lookup and substitution. We have successfully visualized typing derivations for \(\lambda \) calculi with let polymorphism and with shift and reset, System F, as well as a simple deduction system for Combinatory Logic.For the entire collection see [Zbl 1214.68005]. MSC: 68N18 Functional programming and lambda calculus 68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) Keywords:graphical user interface (GUI); proof tree; type system; two-level type; \(\lambda\)-calculus; shift and reset; System F; OCaml; LablTk Software:MikiBeta; PLT Redex; Coq; OCaml PDFBibTeX XMLCite \textit{K. Sakurai} and \textit{K. Asai}, Lect. Notes Comput. Sci. 6564, 84--98 (2011; Zbl 1326.68072) Full Text: DOI References: [1] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. EATCS Series. Springer, Berlin (2004) · Zbl 1069.68095 [2] Danvy, O., Filinski, A.: A Functional Abstraction of Typed Contexts. Technical Report 89/12, DIKU, University of Copenhagen (July 1989) [3] Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT Press, Cambridge (2009) · Zbl 1183.68359 [4] Geuvers, H., Jojgov, G.I.: Open Proofs and Open Terms: A Basis for Interactive Logic. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 537–552. Springer, Heidelberg (2002) · Zbl 1020.03010 [5] Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002) · Zbl 0995.68018 [6] Yakushev, A.R., Holdermans, S., Löh, A., Jeuring, J.: Generic Programming with Fixed Points for Mutually Recursive Datatypes. In: Proceedings of the 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), pp. 233–244 (August 2009) · Zbl 1302.68075 [7] Sheard, T., Pasalic, E.: Two-Level Types and Parameterized Modules. Journal of Functional Programming 14(5), 547–587 (2004) · Zbl 1104.68397 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.