Loading Events

« All Events

  • This event has passed.

[Event canceled] Bucharest FP #61 — Implementing IMP in K and Haskell

March 10, 2020 @ 6:45 pm - 9:00 pm UTC+0

BucharestFP invites you to talk about the contributions to the world of formal verification, using the open-source K framework. RSVP and let’s meet on March 10, starting at 18:45!

 

About the event

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 that 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.

 

About the speaker
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.

 

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

Details

Date:
March 10, 2020
Time:
6:45 pm - 9:00 pm
Event Category:
Event Tags:
, , , , , , ,
Website:
https://www.meetup.com/bucharestfp/events/268949910/

Venue

TechHub Bucharest
District 2, 39-41 Nicolae Filipescu
Bucharest, Romania
+ Google Map
Copyright © TechHub Europe Ltd,