Bucharest FP #61 — Implementing IMP in K and Haskell

Hi, everyone!

It took us a while, but now that the winter's almost done for, we're back.

Our guest for this meetup is a colleague of mine from our US office: Everett Hildenbrandt. He'll be joining us to talk about our contributions to the world of formal verification, using the open-source K framework.

# Everett Hildenbrandt — Side-by-side implementation of an IMP language in K and Haskell

## TALK ABSTRACT
This talk will be a brief introduction to K by example and by comparison with Haskell. We'll start by discussing the programming language IMP, with some demonstrations of programs in this language. Then we'll show how to make an interpreter for this language in Haskell, including a parser and evaluation engine.

Finally, we'll transition to a K interpreter for this language, and show how in addition to an interpreter, K gives a symbolic execution engine which can be used to do program verification. Any remaining time can be used to try things live and for further discussions about what verification is.

## SPEAKER BIO
Everett Hildenbrandt is a Formal Modelling Engineer and Product Owner at Runtime Verification, Inc (a software quality assurance firm). He currently works mostly with KEVM, a K semantics of the Ethereum Virtual Machine (EVM) https://github.com/kframework/evm-semantics. He believes strongly in a semantics-first approach to designing and building the tooling around programming languages.