X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=thesis.bib;fp=thesis.bib;h=468ba5ce4a7e1237beee2d8cc857c618ab1882fa;hb=ffa2d9635d358274433cece34fa326a49794ab62;hp=e8a23d9eaf1e866278d1d32bb224954a38e046cf;hpb=fb4e0b4b2daac3838f6161836298cd4d1bf54766;p=bitonic-mengthesis.git

diff --git a/thesis.bib b/thesis.bib
index e8a23d9..468ba5c 100644
--- a/thesis.bib
+++ b/thesis.bib
@@ -486,4 +486,31 @@ year = {2012}
   pages={348--375},
   year={1978},
   publisher={Elsevier}
+}
+
+@article{dagand2012elaborating,
+  title={Elaborating inductive definitions},
+  author={Dagand, Pierre-Evariste and McBride, Conor},
+  journal={arXiv preprint arXiv:1210.6390},
+  year={2012}
+}
+
+@inproceedings{chapman2010gentle,
+  title={The gentle art of levitation},
+  author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter},
+  booktitle={ACM Sigplan Notices},
+  volume={45},
+  number={9},
+  pages={3--14},
+  year={2010},
+  organization={ACM}
+}
+
+@article{dybjer2000general,
+  title={A general formulation of simultaneous inductive-recursive definitions in type theory},
+  author={Dybjer, Peter},
+  journal={Journal of Symbolic Logic},
+  pages={525--549},
+  year={2000},
+  publisher={JSTOR}
 }
\ No newline at end of file