Skip to content

Instantly share code, notes, and snippets.

@igstan
Last active Feb 28, 2020
Embed
What would you like to do?

Bucharest FP #61 — Implementing IMP in K and Haskell

Event Agenda

  • 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

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.

Registration

Please RSVP on Bucharest FP's meetup page.

Sponsors

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment