agenda

gistfile1.txt

Real world (functional) programming with dependent types!
---------------------------------------------------------
* we want to write a program with /dependent types/
  * shallow embedding vs. deep embedding
* we want to prove some properties of each part of the program
* we need reasoning about programs
  * especially, a program will run correctly
    * interactiton with I/O
    * mutable state
    * etc.
* how to identify some programs which are definitely terminating (pointed out by notogawa-san)
  * avoided the halting problem
    * size change termination/sized type
    * First-Order Unification by Structural Recursion (2001) Conor McBride

---
Pure functional languages with dependent types such as Idris support reasoning about programs directly in the type system,
promising that we can know a program will run correctly (i.e. according to the specification in its type) simply
because it compiles. Realistically, though, things are not so simple: programs have to interact with the outside world,
with user input, input from a network, mutable state, and so on. In this tutorial I will introduce the library,
which is included with the distribution and supports programming and reasoning with side-effecting programs,
supporting mutable state, interaction with the outside world, exceptions, and verified resource management.
--
http://docs.idris-lang.org/en/latest/effects/introduction.html