bamalip: (Default)
(свалка)

ACL2 - doc
Verified programming in F* - source
Theorem Proving in Lean - source
Specifying Systems (TLA+) - source
SPARK 2014 - list
Liquid Haskell - blog
Dafny - github
Twelf - wiki
NURPL - source | amazon
VCC: A Verifier for Concurrent C - home
Z3 - Guide

остальное тут: http://rise4fun.com/
bamalip: (Default)
И не заметил, как свершилось...
Поскольку Идрис, наконец, достиг 1.0, вместе со своей книженцией, то можно теперь спокойно открывать сводные курсы:
"{Coq | Isabelle | Agda | Idris} за 21 день"

Если проводить занятия один день в неделю, и участники будут всю неделю работать над собой, то нормальненько пойдет.


  • Coq


  • Software Foundations - source

    Certified Programming with Dependent Types - amazon | source


  • Isabelle


  • Concrete Semantics - amazon | source

    Isabelle/HOL: A Proof Assistant for Higher-Order Logic - amazon | source


  • Agda


  • Verified Functional Programming in Agda - amazon

    Learn you An Agda And Achieve Enlightenment - source


  • Idris


  • Type-driven Development with Idris - amazon


  • the others


  • Practical Foundations for Programming Languages - amazon | source

    Software Abstractions - amazon | source

    The Little Prover - amazon | source

    Profile

    bamalip: (Default)
    шерстяной ленин

    July 2017

    S M T W T F S
           1
    2 3 4 56 7 8
    9 1011 12 13 14 15
    161718 19 2021 22
    23242526272829
    3031     

    Syndicate

    RSS Atom

    Most Popular Tags

    Style Credit

    Expand Cut Tags

    No cut tags
    Page generated Jul. 22nd, 2017 06:42 pm
    Powered by Dreamwidth Studios