Skip to content
Permalink
Browse files

Added some description of the theory in folder [book].

  • Loading branch information...
rlepigre committed Mar 12, 2019
1 parent 2176d55 commit 7fe8a8e90dd6605ed6332e33888be571bca5fb02
@@ -6,3 +6,10 @@ pml.install
src/config.ml
*/*.merlin
local/
book/pml_book.aux
book/pml_book.bbl
book/pml_book.blg
book/pml_book.log
book/pml_book.out
book/pml_book.pdf
book/pml_book.toc
@@ -30,6 +30,12 @@ bin: src/config.ml
doc:
@dune build @doc

.PHONY: book
book: book/pml_book.pdf

book/pml_book.pdf: book/biblio.bib $(shell find book -name "*.tex")
@cd book && rubber --pdf pml_book.tex

# Configuration file.
src/config.ml: GNUmakefile
@echo "let path = [\"$(LIBDIR)/pml2\"]" > $@
@@ -72,6 +78,7 @@ distclean: clean
@find . -type f -name \#\* -exec rm {} \;
@find . -type f -name .\#\* -exec rm {} \;
@rm -f src/config.ml
@cd book && rubber --clean --pdf pml_book.tex

# Install for the vim mode (in the user's directory).
.PHONY: install_vim
@@ -0,0 +1,121 @@
@phdthesis{Lepigre2017PhD,
author = {Rodolphe Lepigre},
title = {Semantics and Implementation of an Extension of {ML} for Proving Programs.
(S{\'{e}}mantique et Implantation d'une Extension de {ML} pour
la Preuve de Programmes)},
school = {Grenoble Alpes University, France},
year = {2017},
url = {https://tel.archives-ouvertes.fr/tel-01590363}
}

@article{LepRaf2018a,
author = {Lepigre, Rodolphe and Raffalli, Christophe},
title = {Practical Subtyping for Curry-Style Languages},
journal = {ACM Trans. Program. Lang. Syst.},
issue_date = {March 2019},
volume = {41},
number = {1},
month = feb,
year = {2019},
issn = {0164-0925},
pages = {5:1--5:58},
articleno = {5},
numpages = {58},
url = {http://doi.acm.org/10.1145/3285955},
doi = {10.1145/3285955},
acmid = {3285955},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Curry-style quantifiers, Syntax-directed type system, choice
operators, circular proofs, dot notation for abstract types, existential
types, inductive and coinductive sized types, polymorphism, realizability
semantics, reducibility candidates, size change principle, subtyping}
}

@incollection{Parigot1992,
author = {Michel Parigot},
title = {$\lambda\mu$-calculus: An algorithmic interpretation of
classical natural deduction},
booktitle = {Lecture Notes in Computer Science},
volume = {624},
pages = {190--201},
year = {1992},
publisher = {Springer}
}

@inproceedings{Moggi1989,
author = {Eugenio Moggi},
title = {Computational Lambda-Calculus and Monads},
booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science
{(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
pages = {14--23},
publisher = {{IEEE} Computer Society},
year = {1989},
url = {https://doi.org/10.1109/LICS.1989.39155},
doi = {10.1109/LICS.1989.39155},
timestamp = {Wed, 13 Feb 2019 11:42:19 +0100},
biburl = {https://dblp.org/rec/bib/conf/lics/Moggi89},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Flanagan1993,
author = {Cormac Flanagan and
Amr Sabry and
Bruce F. Duba and
Matthias Felleisen},
editor = {Robert Cartwright},
title = {The Essence of Compiling with Continuations},
booktitle = {Proceedings of the {ACM} SIGPLAN'93 Conference on Programming Language
Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June
23-25, 1993},
pages = {237--247},
publisher = {{ACM}},
year = {1993},
url = {https://doi.org/10.1145/155090.155113},
doi = {10.1145/155090.155113},
timestamp = {Tue, 06 Nov 2018 16:59:30 +0100},
biburl = {https://dblp.org/rec/bib/conf/pldi/FlanaganSDF93},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Tarditi1996,
author = {David Tarditi and
J. Gregory Morrisett and
Perry Cheng and
Christopher A. Stone and
Robert Harper and
Peter Lee},
editor = {Charles N. Fischer},
title = {{TIL:} {A} Type-Directed Optimizing Compiler for {ML}},
booktitle = {Proceedings of the {ACM} SIGPLAN'96 Conference on Programming Language
Design and Implementation (PLDI), Philadephia, Pennsylvania, USA,
May 21-24, 1996},
pages = {181--192},
publisher = {{ACM}},
year = {1996},
url = {https://doi.org/10.1145/231379.231414},
doi = {10.1145/231379.231414},
timestamp = {Tue, 06 Nov 2018 16:59:30 +0100},
biburl = {https://dblp.org/rec/bib/conf/pldi/TarditiMCSHL96},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Chlipala2005,
author = {Adam Chlipala and
Leaf Petersen and
Robert Harper},
editor = {J. Gregory Morrisett and
Manuel F{\"{a}}hndrich},
title = {Strict bidirectional type checking},
booktitle = {Proceedings of TLDI'05: 2005 {ACM} {SIGPLAN} International Workshop
on Types in Languages Design and Implementation, Long Beach, CA, USA,
January 10, 2005},
pages = {71--78},
publisher = {{ACM}},
year = {2005},
url = {https://doi.org/10.1145/1040294.1040301},
doi = {10.1145/1040294.1040301},
timestamp = {Tue, 06 Nov 2018 16:58:22 +0100},
biburl = {https://dblp.org/rec/bib/conf/tldi/ChlipalaPH05},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
No changes.
Oops, something went wrong.

0 comments on commit 7fe8a8e

Please sign in to comment.
You can’t perform that action at this time.