New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

WTS: Let's get our hands dirty with code verification #4

Open

pheymann opened this issue Jul 3, 2018 · 0 comments

Labels

Idris type-level verification wts

Member

pheymann commented Jul 3, 2018

type: workshop
audience: intermediate
category: type-level, verification, Idris

Summary

It would be interesting to try code verifications (or proofs) hands-on after we got an introduction in #2.

This workshop could tackle the following problems:

how do we represent data on the type-level
what is equality / inequality
how to proof it

It shouldn't be an introduction into the programming language Idris itself as this would take too long.

pheymann added wts type-level Idris verification labels

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