zchcai/ssft18

Summer School for Formal Techniques

ssft18

Summer School for Formal Techniques

• Main page
• VM for labs

Coq for Type Theory exercises (presented by Stéphane Graham-Lengrand)

• Tutorial
• Run coqide & and open coq/*.v files for exercises.

Agda (presented by Andreas Abel)

• Agda formalization of Categories: https://github.com/InitialTypes/Club (suggested by Abel)
• An intuitionistic theory of types: Predicative part

Ivy (presented by Mooly Sagiv)

• ivy_check is installed in ivy-vm.
• Run ivy_check trace=true debug=true diagnose=true file.ivy.

Rosette (presented by Emina Torlak)

• Steps to run
  • Run drracket to open DrRacket window.
  • Open file sudoku.rkt and click Run.
  • Type (show (generate-puzzle)) and Enter. It will generate a minimal Sudoku puzzle.
  • Open file deep.rkt and click Run.
  • Type (superopt NXp) and Enter. It will synthesize the shortest possible implementation of NXp.
• lab1
  • warmup.rkt
  • sudoku.rkt
• lab2
  • shallow.rkt
  • deep.rkt
• slides: 01, 02

CVC4 (code)

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Racket

Idris

Haskell

State Monad

• Tutorial

Clojure

Prolog (SWI Prolog)

• swipl graph.pl or swipl sudoku.pl
• To exit: ?- halt.