Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Pretty-Printing a Really Long Formula (or, "What a Mathematician Could Learn from Haskell")</h1> <div class='date'><time class="dtstart dt-start" title="2008-09-09T10:30:00" datetime="2008-09-09T10:30:00">Tuesday, September 9, 2008 from 10:30</time>–<time class="dtend dt-end" title="2008-09-09T11:30:00" datetime="2008-09-09T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>TITLE: Pretty-Printing a Really Long Formula (or, "What a Mathematician Could Learn from Haskell")</p> <p>SPEAKER: Lee Pike, R&D Engineering, Galois, Inc.</p> <p>DATE: Tuesday, September 9th. 10.30am</p> <p>LOCATION: <br> Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon</p> <p>ABSTRACT:</p> <p>To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport's brief paper, "How to Write a Long Formula" and "How to Write a Proof" in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.</p> <p>I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I've written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a "HOL Normal Form" for presenting specifications, much like BNF is used for presenting language definitions.</p> <p>BIOGRAPHICAL DETAILS:</p> <p><a href="http://galois.com/company/people/lee_pike/">http://galois.com/company/people/lee_pike/</a></p> <p>ABOUT THE GALOIS TECH TALKS.</p> <p>Galois (<a href="http://galois.com">http://galois.com</a>) has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.</p> <p>The talks are open and free. If you're planning to attend, dropping a note to <a href="mailto:dons@galois.com">dons@galois.com</a> is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers.</p> </div> </div>