monads
所属分类：Coq
开发工具：Coq
文件大小：0KB
下载次数：0
上传日期：2018-10-15 16:52:32
上 传 者：
sh-1993
说明： Coq代码附带了几篇关于函数编程语言语义的文章，
(Coq code accompanying several articles on semantics of functional programming languages,)
文件列表:
monads-trunk/ (0, 2018-10-15)
monads-trunk/AXIOMS/ (0, 2018-10-15)
monads-trunk/AXIOMS/functional_extensionality.v (160, 2018-10-15)
monads-trunk/CAT/ (0, 2018-10-15)
monads-trunk/CAT/CatFunct.v (1859, 2018-10-15)
monads-trunk/CAT/IO.v (16490, 2018-10-15)
monads-trunk/CAT/Misc.v (2369, 2018-10-15)
monads-trunk/CAT/NT.v (3783, 2018-10-15)
monads-trunk/CAT/SO.v (1525, 2018-10-15)
monads-trunk/CAT/bifunctor.v (5243, 2018-10-15)
monads-trunk/CAT/cat_DISCRETE.v (798, 2018-10-15)
monads-trunk/CAT/cat_INDEXED_TYPE.v (13522, 2018-10-15)
monads-trunk/CAT/cat_SET.v (2573, 2018-10-15)
monads-trunk/CAT/cat_TYPE.v (1779, 2018-10-15)
monads-trunk/CAT/cat_TYPE_option.v (811, 2018-10-15)
monads-trunk/CAT/cat_gen_monad.v (3222, 2018-10-15)
monads-trunk/CAT/category.v (3707, 2018-10-15)
monads-trunk/CAT/category_hom_transport.v (2120, 2018-10-15)
monads-trunk/CAT/coproduct.v (5511, 2018-10-15)
monads-trunk/CAT/delta.v (14500, 2018-10-15)
monads-trunk/CAT/enriched_cat.v (2221, 2018-10-15)
monads-trunk/CAT/eq_fibre.v (1685, 2018-10-15)
monads-trunk/CAT/equiv_Monad_MonaD.v (5844, 2018-10-15)
monads-trunk/CAT/free_cats.v (4854, 2018-10-15)
monads-trunk/CAT/functor.v (7006, 2018-10-15)
monads-trunk/CAT/functor_leibniz_eq.v (5388, 2018-10-15)
monads-trunk/CAT/functor_properties.v (1442, 2018-10-15)
monads-trunk/CAT/het_rewrite.v (133, 2018-10-15)
monads-trunk/CAT/horcomp.v (6279, 2018-10-15)
monads-trunk/CAT/ind_potype.v (12841, 2018-10-15)
monads-trunk/CAT/initial_terminal.v (1273, 2018-10-15)
monads-trunk/CAT/ipo_modules.v (5964, 2018-10-15)
monads-trunk/CAT/limits.v (4083, 2018-10-15)
monads-trunk/CAT/module_postcomp_functor.v (1814, 2018-10-15)
monads-trunk/CAT/mon_cats.v (8041, 2018-10-15)
monads-trunk/CAT/monad_def.v (4336, 2018-10-15)
monads-trunk/CAT/monad_h_module.v (13721, 2018-10-15)
monads-trunk/CAT/monad_h_morphism.v (4287, 2018-10-15)
monads-trunk/CAT/monad_h_morphism_gen.v (4174, 2018-10-15)
monads-trunk/CAT/monad_haskell.v (5360, 2018-10-15)
... ...
## COMPILATION
This Coq theory compiles under Coq 8.3pl5, available from https://coq.inria.fr/distrib/V8.3pl5/files/ .
Earlier patch levels should also work; I have tested with 8.3pl2.
Create a Makefile by calling
```bash
$ coq_makefile -f Make > Makefile
```
and compile by calling
```bash
$ make
```
WARNING : The compilation of some of the files consumes up to 2GB of memory. Make sure you dispose of sufficient reserves of ram before compiling the code.
## WORK WITH THE CODE
Call coqide as follows from the root of the library:
```bash
$ coqide -R . CatSem
```
## CONTENT
Read the file "./DESCRIPTION" for a description of the content of each file.
## BRANCHES
Each branch below, printed in **boldface**, corresponds to an article, printed in _italic_.
* [**JFR**](https://github.com/benediktahrens/monads/tree/JFR): [_Initial Semantics for higher-order typed syntax in Coq_](http://jfr.cib.unibo.it/article/view/2066)
* [**MSCS**](https://github.com/benediktahrens/monads/tree/MSCS): [_Modules over relative monads for syntax and semantics_](http://dx.doi.org/10.1017/S0960129514000103)
* [**REDUCTION_RULES**](https://github.com/benediktahrens/monads/tree/REDUCTION_RULES): [_Initial Semantics for Reduction Rules_](http://arxiv.org/abs/1212.5668)
All the articles are also available from my [webpage](http://benedikt-ahrens.de/publications).
近期下载者：
相关文件：
收藏者：