Drawing Trees

Research output: Research - peer-reviewArticle in proceedings – Annual report year: 2018

Documents

View graph of relations

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
Title of host publicationProceedings of the Isabelle Workshop 2018
Number of pages7
Publication date2018
StatePublished - 2018
EventIsabelle Workshop 2018 - Oxford, United Kingdom
Duration: 13 Jul 201813 Jul 2018
http://sketis.net/isabelle/isabelle-workshop-2018

Workshop

WorkshopIsabelle Workshop 2018
CountryUnited Kingdom
CityOxford
Period13/07/201813/07/2018
Internet address
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 149814976