|
Change #12166
2012-01-03
10:19:17
|
create
Calagator::Event
1250461795
Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework
Roll back
| description |
nil |
→ |
Presented by David Lazar
Formal semantics is notoriously hard. The K semantic framework (http://k-framework.org/) 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. |
| end_time |
nil |
→ |
2012-01-10 11:30:00 -0800 |
| id |
nil |
→ |
1250461795 |
| start_time |
nil |
→ |
2012-01-10 10:30:00 -0800 |
| title |
nil |
→ |
Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework |
| url |
nil |
→ |
https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-week-formalizing-haskell-98-in.html |
| venue_id |
nil |
→ |
202390439 |
|