BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:STANDARD DTSTART:20111106T020000 RDATE:20111106T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120103T181917Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T103000 DTSTAMP;VALUE=DATE-TIME:20120103T181917Z LAST-MODIFIED;VALUE=DATE-TIME:20120103T181917Z UID:http://calagator.org/events/1250461795 DESCRIPTION:Presented by David Lazar \;\n \;\nFormal semantics is n otoriously hard. The K semantic framework (http://k-framework.org/) is a system that makes the task of formally defining programming languages e asy 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 co rrectness. These features made it possible to develop a complete formal semantics of the C language in K. \;\nThe 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 gui ding example. The second half of the talk will focus on a work-in-progre ss formalization of Haskell 98 in K. We'll look at the challenges of for malizing Haskell and the applications of this work.\n\nTags: galois\, ha skell\, formal methods\, tech talk\, semantics\n\nImported from: http:// calagator.org/events/1250461795 URL:https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-we ek-formalizing-haskell-98-in.html SUMMARY:Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in t he K Semantic Framework LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR