Index.lagda.rst 1.83 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
================================================================
MPRI 2.4 : Dependently-typed Functional Programming
================================================================



..
  Make sure that everything compiles::

  open import 00-agda.Warmup
  open import 01-effectful.Monad
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
12
  open import 02-dependent.Indexed
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
13
  open import 03-total.Recursion
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
14
  open import 04-generic.Desc
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
15 16 17 18 19 20 21 22 23 24 25 26 27
  open import 05-open.Problems

This course is organized as follows:

.. toctree::
   :maxdepth: 1

   00-agda/Warmup
   01-effectful/Monad
   02-dependent/Indexed
   03-total/Recursion
   04-generic/Desc
   05-open/Problems
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68


************************************************
Contributing
************************************************

Feel free to submit a PR if you spot any typo, have comments or think
of any way to improve the material. For instance, if some resource
available on the web were useful to you during this course, please add
a link to this resource where you see fit.

I also welcome alternative implementations in other dependently-typed
(or almost) languages (OCaml or Haskell with GADTs, vanilla Coq,
Coq/Equations, etc.).

I am also eager to replace references to papers behind paywalls by
freely accessible (but legal and stable) links. Please keep the `doi`_
links in comments nonetheless.

************************************************
Author
************************************************

The lecture notes have been written by `Pierre-Évariste Dagand`_.

************************************************
License
************************************************

These lecture notes are available under an `MIT License`_.


.. References:

.. _`doi`: https://www.doi.org/
.. _`Pierre-Évariste Dagand`: https://pages.lip6.fr/Pierre-Evariste.Dagand/
.. _`MIT License`: https://tldrlegal.com/license/mit-license

.. Local Variables:
.. mode: agda2
.. End: