miniblog.

Sep 29, 2020 at 16:37

Formally verifying a whitespace cleanup editor function in Coq!

Jan 23, 2020 at 04:01

Highlight of #POPL yesterday: seeing some excellent discussions of Coq for verifying programming languages! https://popl20.sigplan.org/details/PLMW-POPL-2020/3/Theorem-provers-are-a-P-L-researcher-s-best-friend I came away with a much clearer sense of *how* you'd verify an optimising compiler.

Theorem provers are a P.L. researcher's best friend (PLMW 2020) - POPL 2020

What is PLMW? The Programming Languages Mentoring Workshop (PLMW) aims to encourage graduate students and senior undergraduate students to pursue careers in programming language research. This workshop will bring together world leaders in programming languages research and teaching from academia and industry to provide (a) technical sessions on cutting-edge PL research and (b) mentoring sessions on how to prepare for a research career. The workshop will engage students in a process of imagining how they might contribute to our research community. We especially encourage women and underrepr ...

Jun 9, 2019 at 16:48

Defining a subset of #[no_std] Rust, formally verifying it, and releasing it as 'Sealed Rust' for use in safety critical systems like automotive and avionics:

Ferrocene

Part 1 - The Pitch

Mar 14, 2018 at 23:27

Given an abundance of information (especially online), we need to be more skilled at verifying the sources and the reputation of the chain of outlets: https://aeon.co/ideas/say-goodbye-to-the-information-age-its-all-about-reputation-now

Related Posts