@@ -1,20 +1,12 @@
11Automatically generated by Mendeley 1.3.1
22Any changes to this file will be lost if it is regenerated by Mendeley.
33
4−@inproceedings{Altenkirch2010,
5−abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
6−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
7−booktitle = {{FLOPS 2010}},
8−doi = {10.1007/978-3-642-12251-4_5},
9−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
10−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
11−isbn = {9783642122507},
12−pages = {40----55},
13−publisher = {Springer Berlin Heidelberg},
14−series = {Lecture Notes in Computer Science},
15−title = {{Dependent Types without the Sugar}},
16−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
17−year = {2010}
4+@article{McBride2006,
5+author = {McBride, C and Goguen, H and McKinna, J},
6+journal = {Types for Proofs and Programs},
7+title = {{A few constructions on constructors}},
8+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
9+year = {2006}
1810}
1911@inproceedings{ko2011modularising,
2012author = {Ko, H.S. and Gibbons, J.},
@@ -464,6 +456,21 @@ title = {{Typing Haskell in Haskell}},
464456url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
465457year = {1999}
466458}
459+@inproceedings{Altenkirch2010,
460+abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
461+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
462+booktitle = {{FLOPS 2010}},
463+doi = {10.1007/978-3-642-12251-4_5},
464+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
465+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
466+isbn = {9783642122507},
467+pages = {40----55},
468+publisher = {Springer Berlin Heidelberg},
469+series = {Lecture Notes in Computer Science},
470+title = {{Dependent Types without the Sugar}},
471+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
472+year = {2010}
473+}
467474@book{Bertot2004,
468475author = {Bertot, Yves and Cast\'{e}ran, Pierre},
469476publisher = {Springer},
@@ -785,13 +792,6 @@ url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
785792volume = {45},
786793year = {2010}
787794}
788−@article{McBride2006,
789−author = {McBride, C},
790−journal = {Types for Proofs and Programs},
791−title = {{A few constructions on constructors}},
792−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
793−year = {2006}
794−}
795795@inproceedings{coquand1986analysis,
796796author = {Coquand, T.},
797797booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},