Drawing Trees

Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen

Research output: Contribution to conferencePaperResearchpeer-review

154 Downloads (Pure)


We formally prove in Isabelle/HOL two properties of an algorithm for laying out trees visually. The first property states that removing layout annotations recovers the original tree. The second property states that nodes are placed at least a unit of distance apart. We have yet to formalize three additional properties: That parents are centered above their children, that drawings are symmetrical with respect to reflection and that identical subtrees are rendered identically.
Original languageEnglish
Publication date2018
Number of pages7
Publication statusPublished - 2018
EventIsabelle Workshop 2018 - Oxford, United Kingdom
Duration: 13 Jul 201813 Jul 2018


WorkshopIsabelle Workshop 2018
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Drawing Trees'. Together they form a unique fingerprint.

Cite this