[Haskell-cafe] ANN: RISC-V ISA Formal Spec (written in Haskell)

[Rishiyur Nikhil]

Title: RISC-V ISA Formal Specification

Speaker: Thomas Bourgeat, MIT
Venue: 8th RISC-V Workshop, Barcelona
Date: Monday May 7, 2018

Abstract: In this tutorial we will demonstrate several flavors of a
    formal specification of the RISC-V ISA, written in Haskell.  We
    will present the important part of the code, use it as a software
    simulator, automatically transform it into a coq specification
    (used to prove the correctness of a small imperative language),
    and automatically synthesize it to circuit (to model check against
    other designs).

    If time permits, we will show how the same code can be used to
    explore some non-determinism in the specification.

Registration info: https://riscv.org/workshops/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180419/e2414ee9/attachment.html>