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)
    шерстяной ленин

    September 2017

    S M T W T F S
          1 2
    3 4 5 6 7 8 9
    1011 12 13 14 1516
    1718 1920212223
    24252627282930

    Syndicate

    RSS Atom

    Most Popular Tags

    Style Credit

    Expand Cut Tags

    No cut tags
    Page generated Sep. 20th, 2017 02:03 am
    Powered by Dreamwidth Studios