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.

abstract:

CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent.

There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and an axiomatic semantics (a separation logic for C). The most important properties — soundness and completeness results, subject reduction and progress, correctness of the type checker — have all been proved. All definitions and proofs have been fully formalized in Coq, without any axioms and on top of a non-trivial support library.

The CH2O project has two abstract C-like languages. A significant subset of C called “CH2O abstract C” is translated into a simplified language called “CH2O core C”. This translation is written in Coq and implicitly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C.

The executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standalone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does not yet support I/O (nor the exit function), a small hack allows the CH2O interpreter to still explore programs that call printf.

The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert and CH2O are that the CH2O semantics has explicit typing judgments for everything, and that CH2O applies to any ISO compliant compiler.

bio:

I have a master degree in mathematics (my thesis was about conformal supergravity), and a PhD in computer science, both from the University of Amsterdam. I also worked as a system administrator at the University of Utrecht.

Currently I’m an assistant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using interactive theorem provers, but recently I have been getting interested in practical program verification, where interactive proof is used when automation doesn’t cut it.

At the moment I am an alternate member of WG14, and I won a price in the IOCCC twice. And my favorite project is the CakeML/verified-HOL Light project.

This month's topic: An Argument for Semantics - Why Developers Should Give a Hoot about OWL

In the push to make use of tagging and other forms user-driven information architectures, developers have overlooked the value of adding semantics, or contextual meaning, directly to the data that powers web sites and applications. The addition of Microformats to a Web site's markup can further the exchange of semantic information such as contact information for people and events. For the most part, however, web sites and applications are still populated by largely non-semantic prose organized in large blocks of HTML or generated from the walled gardens of relational databases and data warehouses.

While everyone agrees that HTML isn't going away anytime soon, several Web Standards have arisen over the last few years to help application developers store, serve, and distribute information with ever-increasing levels of semantics and meaning. The current pinnacle of the Semantic Web Standards pyramid is OWL - the W3C's Web Ontology Language. In this talk I will describe the roots and basics of OWL and how it can be used to power the next generation of smart, data-enabled Web applications.

Speaker: Brian Panulla

Brian is a technology consultant and developer for Dealerpeak - the Portland-based Web-enabled CRM for automotive dealers. A recent transplant to Portland, Brian formerly led grant-funded R&D projects in the information sciences at Penn State University. He moved here primarily for the high quality and variety of beer.

PJUG meetings start with some time to eat and socialize (pizza and beverages are provided), followed by the featured speaker, then Q&A, discussion, sometimes a drawing to give away swag. :)

Though we like knowing how many people to expect, you don't have to RSVP, on Upcoming or otherwise. Go ahead and just show up!

Many people also go for a drink and further discussion following the meeting, at a location determined ad hoc (lately, the Market Street Pub at 10th and Market: http://mcmenamins.com/index.php?loc=24 ).

http://twitter.com/pjug http://pjug.org/ (join our mailing list, linked from the website!)