Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework</h1> <div class='date'><time class="dtstart dt-start" title="2012-01-10T10:30:00" datetime="2012-01-10T10:30:00">Tuesday, January 10, 2012 from 10:30</time>–<time class="dtend dt-end" title="2012-01-10T11:30:00" datetime="2012-01-10T11: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>Presented by David Lazar</p> <p>Formal semantics is notoriously hard. The K semantic framework (<a href="http://k-framework.org/">http://k-framework.org/</a>) is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K. The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-week-formalizing-haskell-98-in.html">Website</a></li> </ul> </div>