2 author = {Thompson, Simon},
3 title = {Type Theory and Functional Programming},
4 publisher = {Addison-Wesley},
9 author = {Pierce, Benjamin C.},
10 title = {Types and Programming Languages},
11 publisher = {The MIT Press},
16 author = {{The Coq Team}},
17 title = {The Coq Proof Assistant},
18 url = {\url{coq.inria.fr}},
19 howpublished = {\url{http://coq.inria.fr}},
24 author = {{The GHC Team}},
25 title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
26 url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
27 howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
32 author = {Conor McBride},
33 title = {Epigram: Practical Programming with Dependent Types},
34 url = {http://strictlypositive.org/epigram-notes.ps.gz},
35 howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
40 author = {Simon Marlow},
41 title = {Haskell 2010, Language Report},
42 url = {http://www.haskell.org/onlinereport/haskell2010/},
43 howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
48 author = {Miran Lipova\v{c}a},
49 title = {Learn You a Haskell for Great Good!},
50 url = {http://learnyouahaskell.com/},
51 howpublished = {\url{http://learnyouahaskell.com/}},
56 author = {Graham Hutton},
57 title = {Programming in Haskell},
59 publisher = {Cambridge University Press}
63 author = {Robert L. Constable and the PRL Group},
64 title = {Implementing Mathematics with The NuPRL Proof Development System},
66 publisher = Prentice-Hall
70 @article{Altenkirch2010,
71 author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
72 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
73 journal = {Functional and Logic \ldots},
74 number = {Sheard 2005},
75 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
76 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
79 @article{Altenkirch2007,
80 address = {New York, New York, USA},
81 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
82 doi = {10.1145/1292597.1292608},
83 file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
84 isbn = {9781595936776},
85 journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
86 keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
88 publisher = {ACM Press},
89 title = {{Observational equality, now!}},
90 url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
93 @article{Barendregt1991,
94 author = {Barendregt, Henk},
95 file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
96 journal = {Journal of functional programming},
97 title = {{Introduction to generalized type systems}},
98 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
102 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
103 file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
104 journal = {Theorem Proving in Higher Order Logics},
105 title = {{A brief overview of Agda - a functional language with dependent types}},
106 url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
110 author = {Brady, Edwin},
111 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
112 journal = {Unpublished draft},
114 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
115 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
118 @article{Chapman2010,
119 address = {New York, New York, USA},
120 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
121 doi = {10.1145/1863543.1863547},
122 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
123 isbn = {9781605587943},
124 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
126 publisher = {ACM Press},
127 title = {{The gentle art of levitation}},
128 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
132 author = {Church, Alonzo},
133 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
134 journal = {American journal of mathematics},
137 title = {{An unsolvable problem of elementary number theory}},
138 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
143 author = {Church, Alonzo},
144 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
145 journal = {J. Symb. Log.},
148 title = {{A formulation of the simple theory of types}},
149 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
153 @article{Coquand1986,
154 author = {Coquand, Thierry and Huet, Gerard},
155 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
156 title = {{The calculus of constructions}},
157 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
161 author = {Curry, Haskell B.},
162 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
163 journal = {Proceedings of the National Academy of Sciences of the United States of America},
166 title = {{Functionality in combinatory logic}},
167 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
172 author = {Dybjer, Peter},
173 file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
174 journal = {Logical Frameworks},
175 title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
176 url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
179 @article{Hurkens1995,
180 author = {Hurkens, Antonius J.C.},
181 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
182 journal = {Typed Lambda Calculi and Applications},
183 title = {{A simplification of Girard's paradox}},
184 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
188 author = {Jacobs, Bart and Rutten, Jan},
189 file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf},
190 journal = {EATCS Bulletin},
192 title = {{A tutorial on (co) algebras and (co) induction}},
193 url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf},
197 @book{Martin-Lof1984,
198 author = {Martin-L\"{o}f, Per},
199 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
201 publisher = {Bibliopolis},
202 title = {{Intuitionistic type theory}},
205 @article{McBride2004,
206 author = {McBride, Conor},
207 doi = {10.1017/S0956796803004829},
208 file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
209 journal = {Journal of Functional Programming},
213 title = {{The View from The Left}},
214 url = {http://strictlypositive.org/view.ps.gz},
218 @phdthesis{Norell2007,
219 author = {Norell, Ulf},
220 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
221 isbn = {9789172919969},
222 school = {Chalmers University of Technology and G\"{o}teborg University},
223 title = {{Towards a practical programming language based on dependent type theory}},
224 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
228 address = {New York, New York, USA},
229 author = {Oury, Nicolas and Swierstra, Wouter},
230 doi = {10.1145/1411204.1411213},
231 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
232 isbn = {9781595939197},
233 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
235 publisher = {ACM Press},
236 title = {{The power of Pi}},
237 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
241 author = {Pierce, Benjamin C. and Turner, David N.},
242 doi = {10.1145/345099.345100},
243 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
245 journal = {ACM Transactions on Programming Languages and Systems},
249 title = {{Local type inference}},
250 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
254 @article{Pollack1990,
255 author = {Pollack, Robert},
256 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
257 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
258 title = {{Implicit syntax}},
259 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
262 @article{Reynolds1994,
263 author = {Reynolds, John C.},
264 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
265 journal = {Logical Foundations of Functional Programming},
266 title = {{An introduction to the polymorphic lambda calculus}},
267 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
270 @article{Sulzmann2007,
271 address = {New York, New York, USA},
272 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
273 doi = {10.1145/1190315.1190324},
274 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
276 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
278 publisher = {ACM Press},
279 title = {{System F with type equality coercions}},
280 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
283 @article{Vytiniotis2011,
284 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
285 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
286 journal = {Journal of Functional Programming},
289 title = {{OutsideIn (X) Modular type inference with local assumptions}},
290 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
295 address = {New York, New York, USA},
296 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
297 doi = {10.1145/2103786.2103795},
298 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
299 isbn = {9781450311205},
300 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
302 publisher = {ACM Press},
303 title = {{Giving Haskell a promotion}},
304 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
307 @phdthesis{McBride1999,
308 author = {McBride, Conor},
309 file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf},
310 school = {University of Edinburgh},
311 title = {{Dependently typed functional programs and their proofs}},
312 url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},