Bucharest FP #61 — Implementing IMP in K and Haskell
- 18:45 — 19:00 Welcome
- 19:00 — 20:00 Everett Hildenbrandt — Side-by-side implementation of an IMP language in K and Haskell
- 20:00 — 21:00 Networking
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.
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.
This event is hosted through TechSociety, an initiative that aims to grow the local tech community stronger by providing free event space, as well as logistical and communication support, to all people that organize free tech-related events.
Thinking about organizing a meetup or an event for the tech community out there? Join TechSociety and we’ll help you out! All you have to do is submit the registration form available on our website, and we’ll get back to you to set all the details straight!