How to Pretty-Print a Long Formula

• ABSTRACT:
  
  We present a standard rendering for higher-order logic (HOL) to make specifications more readable. We propose a structured rendering that borrows greatly from Leslie Lamport's original proposal for writ- ing long mathematical formulas. Furthermore, we present a freely- available parser and pretty-printer that implements these ideas, which we call beautifHOL. We conclude by describing possible extensions to our proposed rendering and motivate the need for formatting standards for formal specifications.

• BIBTEX:
  

  @misc{pike-pp,
    author =    {Lee Pike},
    title =     {How to pretty-print a long formula},
    note =      {Unpublished.  Available at \url{https://leepike.github.io/pub_pages/holpp.html}}}
  

• PAPER DOWNLOAD: pdf 

• SLIDES DOWNLOAD: To appear.

• PROGRAM DOWNLOAD: The pretty-printer, called beautifHOL, is written in Haskell and is available for download from Hackage, which provides facilities to automatically build and install Haskell programs.

• OTHER FILES:
  
  
  • Documentation (HTML)
  • README
  • LICENSE (BSD3 license)
  • BNF grammar specification of the input language: pdf
  • Test data (file of input formulas): examples.txt.
    Issue beautifHOL --f formulas.txt to pretty-print every uncommented formula in the file..