3 author = {Thompson, Simon},
4 title = {Type Theory and Functional Programming},
5 publisher = {Addison-Wesley},
10 author = {Pierce, Benjamin C.},
11 title = {Types and Programming Languages},
12 publisher = {The MIT Press},
17 author = {{The Coq Team}},
18 title = {The Coq Proof Assistant},
19 url = {\url{coq.inria.fr}},
20 howpublished = {\url{http://coq.inria.fr}},
25 author = {{The GHC Team}},
26 title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
27 url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
28 howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
33 author = {Conor McBride},
34 title = {Epigram: Practical Programming with Dependent Types},
35 url = {http://strictlypositive.org/epigram-notes.ps.gz},
36 howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
41 author = {Simon Marlow},
42 title = {Haskell 2010, Language Report},
43 url = {http://www.haskell.org/onlinereport/haskell2010/},
44 howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
49 author = {Miran Lipova\v{c}a},
50 title = {Learn You a Haskell for Great Good!},
51 url = {http://learnyouahaskell.com/},
52 howpublished = {\url{http://learnyouahaskell.com/}},
57 author = {Graham Hutton},
58 title = {Programming in Haskell},
60 publisher = {Cambridge University Press}
65 author = {Constable, Robert L. and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith},
66 title = {Implementing Mathematics with the NuPRL Proof Development System},
68 publisher = {Prentice-Hall},
73 @article{Altenkirch2010,
74 author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
75 file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
76 journal = {Functional and Logic \ldots},
77 number = {Sheard 2005},
78 title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
79 url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
82 @article{Altenkirch2007,
83 address = {New York, New York, USA},
84 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
85 doi = {10.1145/1292597.1292608},
86 file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
87 isbn = {9781595936776},
88 journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
89 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},
91 publisher = {ACM Press},
92 title = {{Observational equality, now!}},
93 url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
96 @article{Barendregt1991,
97 author = {Barendregt, Henk},
98 file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
99 journal = {Journal of functional programming},
100 title = {{Introduction to generalized type systems}},
101 url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
105 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
106 file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
107 journal = {Theorem Proving in Higher Order Logics},
108 title = {{A brief overview of Agda - a functional language with dependent types}},
109 url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
113 author = {Brady, Edwin},
114 file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
115 journal = {Unpublished draft},
117 title = {{Implementing General Purpose Dependently Typed Programming Languages}},
118 url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
121 @article{Chapman2010,
122 address = {New York, New York, USA},
123 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
124 doi = {10.1145/1863543.1863547},
125 file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
126 isbn = {9781605587943},
127 journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
129 publisher = {ACM Press},
130 title = {{The gentle art of levitation}},
131 url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
135 author = {Church, Alonzo},
136 file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
137 journal = {American journal of mathematics},
140 title = {{An unsolvable problem of elementary number theory}},
141 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
146 author = {Church, Alonzo},
147 file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
148 journal = {J. Symb. Log.},
151 title = {{A formulation of the simple theory of types}},
152 url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
156 @article{Coquand1986,
157 author = {Coquand, Thierry and Huet, Gerard},
158 file = {:home/bitonic/docs/papers/coc.pdf:pdf},
159 title = {{The calculus of constructions}},
160 url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
164 author = {Curry, Haskell B.},
165 file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
166 journal = {Proceedings of the National Academy of Sciences of the United States of America},
169 title = {{Functionality in combinatory logic}},
170 url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
175 author = {Dybjer, Peter},
176 file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
177 journal = {Logical Frameworks},
178 title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
179 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},
182 @article{Hurkens1995,
183 author = {Hurkens, Antonius J.C.},
184 file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
185 journal = {Typed Lambda Calculi and Applications},
186 title = {{A simplification of Girard's paradox}},
187 url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
190 @book{Martin-Lof1984,
191 author = {Martin-L\"{o}f, Per},
192 file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
194 publisher = {Bibliopolis},
195 title = {{Intuitionistic type theory}},
198 @article{McBride2004,
199 author = {McBride, Conor},
200 doi = {10.1017/S0956796803004829},
201 file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
202 journal = {Journal of Functional Programming},
206 title = {{The View from The Left}},
207 url = {http://strictlypositive.org/view.ps.gz},
211 @phdthesis{Norell2007,
212 author = {Norell, Ulf},
213 file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
214 isbn = {9789172919969},
215 school = {Chalmers University of Technology and G\"{o}teborg University},
216 title = {{Towards a practical programming language based on dependent type theory}},
217 url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
221 address = {New York, New York, USA},
222 author = {Oury, Nicolas and Swierstra, Wouter},
223 doi = {10.1145/1411204.1411213},
224 file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
225 isbn = {9781595939197},
226 journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
228 publisher = {ACM Press},
229 title = {{The power of Pi}},
230 url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
234 author = {Pierce, Benjamin C. and Turner, David N.},
235 doi = {10.1145/345099.345100},
236 file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
238 journal = {ACM Transactions on Programming Languages and Systems},
242 title = {{Local type inference}},
243 url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
247 @article{Pollack1990,
248 author = {Pollack, Robert},
249 file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
250 journal = {Informal Proceedings of First Workshop on Logical Frameworks},
251 title = {{Implicit syntax}},
252 url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
255 @article{Reynolds1994,
256 author = {Reynolds, John C.},
257 file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
258 journal = {Logical Foundations of Functional Programming},
259 title = {{An introduction to the polymorphic lambda calculus}},
260 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
263 @article{Sulzmann2007,
264 address = {New York, New York, USA},
265 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
266 doi = {10.1145/1190315.1190324},
267 file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
269 journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
271 publisher = {ACM Press},
272 title = {{System F with type equality coercions}},
273 url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
276 @article{Vytiniotis2011,
277 author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
278 file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
279 journal = {Journal of Functional Programming},
282 title = {{OutsideIn (X) Modular type inference with local assumptions}},
283 url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
288 address = {New York, New York, USA},
289 author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
290 doi = {10.1145/2103786.2103795},
291 file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
292 isbn = {9781450311205},
293 journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
295 publisher = {ACM Press},
296 title = {{Giving Haskell a promotion}},
297 url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},