-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
499 lines (499 loc) · 25.3 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="generator" content="pandoc">
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
<title>A Type Theory Reading Group</title>
<style type="text/css">code{white-space: pre;}</style>
<link rel="stylesheet" href="main.css">
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
</head>
<body>
<header>
<h1 class="title">A Type Theory Reading Group</h1>
</header>
<nav id="TOC">
<ul>
<li><a href="#meetings">Meetings</a><ul>
<li><a href="#spring-2018">Spring 2018</a></li>
<li><a href="#fall-2017">Fall 2017</a></li>
<li><a href="#spring-2017">Spring 2017</a></li>
<li><a href="#fall-2016">Fall 2016</a></li>
<li><a href="#summer-2016">Summer 2016</a></li>
<li><a href="#spring-2016">Spring 2016</a></li>
</ul></li>
<li><a href="#topics">Topics</a><ul>
<li><a href="#history-philosophy">History & Philosophy</a></li>
<li><a href="#datatypes">Datatypes</a></li>
<li><a href="#coinduction">Coinduction</a></li>
<li><a href="#meaning-explanations">Meaning Explanations</a></li>
<li><a href="#description-techniques">Description Techniques</a></li>
<li><a href="#implementation-techniques">Implementation Techniques</a></li>
<li><a href="#implementations">Implementations</a></li>
<li><a href="#alternatives">Alternatives</a></li>
<li><a href="#find-the-right-papers-for-these"><span class="todo TODO">TODO</span> Find the right papers for these</a></li>
</ul></li>
</ul>
</nav>
<p>The group will meet weekly, also during the summers, for a period of one hour. Everyone has the responsibility to read the material before arriving, but one person will have the responsibility of being in solid command of it and presenting it as a discussion starter.</p>
<p>Tori/Vikraman is responsible for booking rooms and taking care of the administrative work.</p>
<h1 id="meetings">Meetings</h1>
<h2 id="spring-2018">Spring 2018</h2>
<p>Tuesdays 12-1PM, Luddy Hall 3069</p>
<h3 id="tuesday-6-march-2018">Tuesday, 6 March, 2018</h3>
<ul>
<li><a href="http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf">Locally cartesian closed categories and type theory</a> by R. A. G. Seely</li>
</ul>
<h3 id="tuesday-20-february-2018">Tuesday, 20 February, 2018</h3>
<ul>
<li><a href="http://conal.net/papers/compiling-to-categories/">Compiling to Categories</a> (contd.)</li>
</ul>
<h3 id="tuesday-13-february-2018">Tuesday, 13 February, 2018</h3>
<ul>
<li><a href="http://conal.net/papers/compiling-to-categories/">Compiling to Categories</a> (contd.)</li>
</ul>
<h3 id="tuesday-6-february-2018">Tuesday, 6 February, 2018</h3>
<ul>
<li><a href="http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf">Compiling to Categories</a> by Conal Elliott</li>
<li><a href="http://conal.net/papers/compiling-to-categories/">Paper website</a></li>
</ul>
<h3 id="tuesday-30-january-2018">Tuesday, 30 January, 2018</h3>
<ul>
<li>CANCELLED (everyone's sick)</li>
</ul>
<h3 id="tuesday-23-january-2018">Tuesday, 23 January, 2018</h3>
<ul>
<li>Planning meeting</li>
</ul>
<h2 id="fall-2017">Fall 2017</h2>
<h3 id="monday-4-december-2017">Monday, 4 December, 2017</h3>
<ul>
<li>Tori Lewis</li>
<li><a href="https://link.springer.com/chapter/10.1007/3-540-45413-6_11">Ramified Recurrence with Dependent Types</a> by Norman Danner</li>
<li><a href="https://goo.gl/vrbWug">Un-paywalled link</a></li>
</ul>
<h3 id="monday-27-november-2017">Monday, 27 November, 2017</h3>
<ul>
<li>Hamidreza Bahramian</li>
<li><a href="http://hdl.handle.net/2022/21811">Copredication in homotopy type theory</a> by Hamidreza Bahramian, Narges Nematollahi, and Amr Sabry</li>
</ul>
<h3 id="monday-13-november-2017">Monday, 13 November, 2017</h3>
<ul>
<li>No meeting</li>
</ul>
<h3 id="monday-6-november-2017">Monday, 6 November, 2017</h3>
<ul>
<li>Ryan Scott presenting AND organizing</li>
<li><a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/coercible.pdf">Safe Zero-cost Coercions for Haskell</a> by Breitner, Eisenberg, Peyton Jones, and Weirich</li>
</ul>
<h3 id="monday-30-october-2017">Monday, 30 October, 2017</h3>
<ul>
<li>No meeting</li>
</ul>
<h3 id="monday-23-october-2017">Monday, 23 October, 2017</h3>
<ul>
<li>Tori Lewis</li>
<li><a href="http://www.cse.chalmers.se/~peterd/papers/Finite_IR.pdf">A Finite Axiomatization of Inductive-Recursive Definitions</a> by Dybjer and Setzer</li>
</ul>
<h3 id="monday-16-october-2017">Monday, 16 October, 2017</h3>
<ul>
<li>David Christiansen</li>
<li><a href="https://jmchapman.github.io/papers/levitation.pdf">The Gentle Art of Levitation</a> by Chapman, Dagand, McBride, and Morris</li>
</ul>
<h3 id="monday-9-october-2017">Monday, 9 October, 2017</h3>
<ul>
<li>Chao-Hong Chen</li>
</ul>
<h3 id="monday-2-october-2017">Monday, 2 October, 2017</h3>
<ul>
<li>Tori Lewis</li>
</ul>
<h3 id="monday-25-september-2017">Monday, 25 September, 2017</h3>
<ul>
<li>David Christiansen</li>
<li><a href="http://www.cs.swan.ac.uk/~csetzer/articles/iopreprint.pdf">Interactive Programs in Dependent Type Theory</a> by Peter Hancock and Anton Setzer</li>
</ul>
<h3 id="monday-18-september-2017---meeting-canceled">Monday, 18 September, 2017 - Meeting canceled</h3>
<ul>
<li>Vikraman Choudhury</li>
<li>Appendix B from <a href="https://arxiv.org/pdf/1606.05916.pdf">Guillaume Brunerie's thesis</a>: The cardinal of π₄(𝕊³)</li>
</ul>
<h3 id="monday-11-september-2017">Monday, 11 September, 2017</h3>
<ul>
<li>Ryan Scott</li>
<li>Presenting Chapter 4 from <a href="https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf">Richard Eisenberg's thesis</a> (pp 51--66)</li>
</ul>
<h3 id="monday-4-september-2017">Monday, 4 September, 2017</h3>
<ul>
<li>US Labor Day and ICFP, no meeting</li>
</ul>
<h3 id="monday-28-august-2017">Monday, 28 August, 2017</h3>
<ul>
<li>Planning meeting in THE ABYSS</li>
</ul>
<h2 id="spring-2017">Spring 2017</h2>
<h3 id="monday-1-may-2017">Monday, 1 May, 2017</h3>
<h3 id="monday-24-april-2017">Monday, 24 April, 2017</h3>
<ul>
<li>David Christiansen</li>
<li><a href="http://pauillac.inria.fr/~herbelin/articles/tlca-Her05-callcc-sigma-types.pdf">On the Degeneracy of Σ-Types in Presence of Computational Classical Logic</a> by Hugo Herbelin</li>
</ul>
<h3 id="monday-17-april-2017">Monday, 17 April, 2017</h3>
<ul>
<li>No meeting</li>
</ul>
<h3 id="monday-10-april-2017">Monday, 10 April, 2017</h3>
<ul>
<li>Chao-Hong Chen</li>
<li><a href="http://www.cs.bham.ac.uk/~mhe/papers/escardo-xu-inconsistency-continuity.pdf">The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation</a> by Martín Escardó and Chuangjie Xu</li>
</ul>
<h3 id="monday-3-april-2017">Monday, 3 April, 2017</h3>
<ul>
<li>Vikraman Choudhury</li>
<li><a href="https://www.cs.cmu.edu/~drl/pubs/lh112tt/lh122tt-final.pdf">Canonicity for 2-Dimensional Type Theory</a> by Dan Licata and Bob Harper</li>
</ul>
<h3 id="monday-27-march-2017">Monday, 27 March, 2017</h3>
<ul>
<li>David Christiansen</li>
<li><em>Epigram Reloaded: A Standalone Typechecker for ETT</em> by James Chapman, Thorsten Altenkirch, and Conor McBride</li>
</ul>
<h3 id="monday-20-march-2017">Monday, 20 March, 2017</h3>
<ul>
<li>Tori Lewis</li>
<li><a href="http://www.nuprl.org/html/Nuprl2Coq/continuity.pdf">A Nominal Exploration of Intuitionism</a> by Vincent Rahli and Mark Bickford</li>
</ul>
<h3 id="monday-13-march-2017">Monday, 13 March, 2017</h3>
<ul>
<li>No meeting, Spring Break</li>
</ul>
<h3 id="monday-6-march-2017">Monday, 6 March, 2017</h3>
<ul>
<li>Robert Rose</li>
<li><a href="http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz">The Groupoid Interpretation of Type Theory</a> by Martin Hofmann and Thomas Streicher (continuing from last week)</li>
</ul>
<h3 id="monday-27-february-2017">Monday, 27 February, 2017</h3>
<ul>
<li>Robert Rose</li>
<li><a href="http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz">The Groupoid Interpretation of Type Theory</a> by Martin Hofmann and Thomas Streicher</li>
</ul>
<h3 id="monday-20-february-2017---canceled">Monday, 20 February, 2017 - CANCELED</h3>
<h3 id="monday-13-february-2017">Monday, 13 February, 2017</h3>
<ul>
<li>Weixi Ma</li>
<li><a href="http://www.cse.chalmers.se/~peterd/papers/Testing_Proving.pdf">Combining testing and proving in dependent type theory</a> by Peter Dybjer, Qiao Haiyan, and Makoto Takeyama</li>
</ul>
<h3 id="monday-6-february-2017">Monday, 6 February, 2017</h3>
<ul>
<li>David Christiansen</li>
<li><a href="papers/afpr.pdf">Algebraic Foundations of Proof Refinement</a> by Jonathan Sterling and Robert Harper</li>
</ul>
<h3 id="monday-30-january-2017">Monday, 30 January, 2017</h3>
<ul>
<li>Kyle Carter</li>
<li><a href="https://arxiv.org/abs/1701.02571">Stack Semantics of Type Theory</a> by Thierry Coquand, Bassel Mannaa, and Fabian Ruch</li>
</ul>
<h3 id="monday-23-january-2017">Monday, 23 January, 2017</h3>
<ul>
<li>Planning meeting</li>
<li>Decision: we stick to Mondays at 11</li>
</ul>
<h2 id="fall-2016">Fall 2016</h2>
<h3 id="monday-19-december-2016">Monday, 19 December, 2016</h3>
<ul>
<li>No meeting due to winter break.</li>
</ul>
<h3 id="monday-12-december-2016">Monday, 12 December, 2016</h3>
<ul>
<li>Control operators and types pt 2</li>
<li>Reading: <a href="http://www.cs.indiana.edu/~sabry/papers/contFoundationLong.pdf" class="uri">http://www.cs.indiana.edu/~sabry/papers/contFoundationLong.pdf</a></li>
<li>Presenting: Amr Sabry</li>
<li>Finals week.</li>
</ul>
<h3 id="monday-5-december-2016">Monday, 5 December, 2016</h3>
<ul>
<li>Contextual Isomorphisms</li>
<li><a href="https://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf" class="uri">https://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf</a></li>
<li>Presenting: Vikraman Choudhury</li>
</ul>
<h3 id="monday-28-november-2016">Monday, 28 November, 2016</h3>
<ul>
<li>Control operators and types pt 1</li>
<li><a href="http://www.cs.indiana.edu/~sabry/papers/foundationAbortive-TR.pdf" class="uri">http://www.cs.indiana.edu/~sabry/papers/foundationAbortive-TR.pdf</a> esp. sections 1-3</li>
<li>Presenting: Amr Sabry</li>
<li><a href="extra/C.agda">Agda code from talk</a></li>
</ul>
<h3 id="monday-21-november-2016">Monday, 21 November, 2016</h3>
<ul>
<li>US Thanksgiving week, so no meeting.</li>
</ul>
<h3 id="monday-14-november-2016">Monday, 14 November, 2016</h3>
<ul>
<li>"Löb’s Theorem: A functional pearl of dependently typed quining" by Jason Gross, Jack Gallagher, and Benya Fallenstein.</li>
<li><a href="https://jasongross.github.io/lob-paper/nightly/lob.pdf" class="uri">https://jasongross.github.io/lob-paper/nightly/lob.pdf</a></li>
<li>Presenting: Weixi Ma</li>
</ul>
<h3 id="monday-7-november-2016">Monday, 7 November, 2016</h3>
<ul>
<li>Planning meeting.</li>
</ul>
<h3 id="monday-24-october-2016">Monday, 24 October, 2016</h3>
<ul>
<li>"Truth of a proposition, evidence of a judgement, validity of a proof" by Per Martin-Löf. Synthese 73(3), pp. 407--420. 1987.</li>
<li><a href="https://michaelt.github.io/martin-lof/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf" class="uri">https://michaelt.github.io/martin-lof/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf</a></li>
<li>Presenting: David Christiansen</li>
</ul>
<h3 id="monday-24-october-2016-1">Monday, 24 October, 2016</h3>
<ul>
<li>"Observational Equality, Now!" by Thorsten Altenkirch, Conor McBride, and Wouter Swierstra.</li>
<li><a href="http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf" class="uri">http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf</a></li>
<li>Presenting: David Christiansen</li>
</ul>
<h3 id="monday-17-october-2016">Monday, 17 October, 2016</h3>
<ul>
<li>No reading. Instead, we will have a discussion session on formalizing category theory, lead by Tang Jiawei.</li>
</ul>
<h3 id="monday-10-october-2016">Monday, 10 October, 2016</h3>
<ul>
<li>Reading: "Denotation of Contextual Modal Type Theory (CMTT): syntax and metaprogramming" by Murdoch J. Gabbay and Aleksandar Nanevski</li>
<li>Available <a href="http://gabbay.org.uk/papers/dencmt.pdf">from author</a></li>
<li>Presenting: Kyle Carter</li>
</ul>
<h3 id="monday-3-october-2016">Monday, 3 October, 2016</h3>
<ul>
<li>Reading: "Unifiers as equivalences: proof-relevant unification of dependently typed data" by Cockx, Devriese, and Piessens</li>
<li>Available on <a href="http://dl.acm.org/citation.cfm?id%3D2951917&CFID%3D844154474&CFTOKEN%3D48082776">ACM DL</a></li>
<li>Presenting: David Christiansen</li>
</ul>
<h3 id="monday-26-september-2016">Monday, 26 September, 2016</h3>
<h3 id="monday-19-september-2016">Monday, 19 September, 2016</h3>
<ul>
<li>Reading: "Constructing Type Systems over an Operational Semantics" by Bob Harper.</li>
<li><a href="https://www.cs.uoregon.edu/research/summerschool/summer10/lectures/Harper-JSC92.pdf">PDF</a></li>
<li>Presenting: Tori Lewis</li>
</ul>
<h3 id="monday-12-september-2016">Monday, 12 September, 2016</h3>
<ul>
<li>Cancelled due to illness</li>
</ul>
<h3 id="monday-5-september-2016">Monday, 5 September, 2016</h3>
<ul>
<li>U.S. Labor Day. No meeting.</li>
</ul>
<h3 id="monday-29-august-2016">Monday, 29 August, 2016</h3>
<ul>
<li>Talk by Edwin Brady. No reading.</li>
</ul>
<h3 id="monday-22-august-2016">Monday, 22 August, 2016</h3>
<ul>
<li>Reading: "The Power of Pi" by Nicolas Oury and Wouter Swierstra</li>
<li><a href="http://www.staff.science.uu.nl/~swier004/Publications/ThePowerOfPi.pdf">PDF</a></li>
<li>Presenting: Chaitainya Koparkar</li>
</ul>
<h2 id="summer-2016">Summer 2016</h2>
<h3 id="monday-15-august-2016">Monday, 15 August, 2016</h3>
<ul>
<li>Reading: "Continuity of Gödel’s system T definable functionals via effectful forcing" by Martín Escardó</li>
<li><a href="http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf">PDF</a></li>
<li>Presenting: Jon Sterling</li>
</ul>
<h3 id="monday-8-august-2016">Monday, 8 August, 2016</h3>
<ul>
<li>Reading: "Homotopy theoretic models of identity types" by Steve Awodey and Michael A. Warren.</li>
<li><a href="http://arxiv.org/abs/0709.0248">PDF</a></li>
<li>Presenting: Hamidreza Bahramian</li>
</ul>
<h3 id="monday-1-august-2016">Monday, 1 August, 2016</h3>
<ul>
<li>Cancelled</li>
</ul>
<h3 id="monday-25-july-2016">Monday, 25 July, 2016</h3>
<ul>
<li>Reading: "Computational Higher-Dimensional Type Theory" by Carlo Angiuli, Robert Harper, and Todd Wilson.</li>
<li><a href="http://www.cs.cmu.edu/~rwh/papers/chitt/draft.pdf">PDF</a></li>
<li>Presenting: David Christiansen</li>
</ul>
<h3 id="monday-18-july-2016">Monday, 18 July, 2016</h3>
<ul>
<li>Reading: "Cubical Type Theory: a constructive interpretation of the univalence axiom" by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg</li>
<li><a href="https://www.math.ias.edu/~amortberg/papers/cubicaltt.pdf">PDF</a></li>
<li>Presenting: Tim Zakian</li>
</ul>
<h3 id="monday-11-july-2016">Monday, 11 July, 2016</h3>
<ul>
<li>Reading: "Ornamental Algebras, Algebraic Ornaments" by Conor McBride.</li>
<li><a href="https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf">PDF</a></li>
<li>Presenting: Jason Hemann</li>
<li><strong>Change of venue:</strong> LH 325</li>
</ul>
<h3 id="monday-4-july-2016">Monday, 4 July, 2016</h3>
<p>Cancelled due to U.S. Independence Day.</p>
<h3 id="monday-27-june-2016">Monday, 27 June, 2016</h3>
<ul>
<li>Reading: "Outrageous but Meaningful Coincidences" by Conor McBride.</li>
<li><a href="https://personal.cis.strath.ac.uk/conor.mcbride/pub/DepRep/DepRep.pdf">PDF</a></li>
<li>Presenting: Kyle Carter</li>
</ul>
<h3 id="monday-20-june-2016">Monday, 20 June, 2016</h3>
<ul>
<li>Reading: "Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation" by Edwin Brady. In Journal of Functional Programming, October 2013.</li>
<li><a href="http://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf">PDF</a></li>
<li>Presenting: Rajan Walia</li>
</ul>
<h3 id="monday-13-june-2016">Monday, 13 June, 2016</h3>
<ul>
<li>Reading: "Indexed Containers" by Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. In LICS 2009.
<ul>
<li><a href="http://strictlypositive.org/indexed-containers.pdf">PDF</a></li>
</ul></li>
<li>Presenting: Larry Moss</li>
</ul>
<h3 id="monday-6-june-2016">Monday, 6 June, 2016</h3>
<ul>
<li>Reading: "Pattern matching with dependent types" by Thierry Coquand. From a 1992 workshop at Båstad.
<ul>
<li><a href="http://www.lfcs.inf.ed.ac.uk/research/types-bra/proc/proc92.ps.gz">Original proceedings</a></li>
<li><a href="papers/proc92.pdf">PDF version of proceedings</a></li>
<li><a href="papers/proc92-coquand.pdf">PDF of just the paper</a></li>
</ul></li>
<li>Presenting: Andrew Kent</li>
</ul>
<h3 id="monday-30-may-2016">Monday, 30 May, 2016</h3>
<p>Cancelled due to Memorial Day.</p>
<h3 id="monday-23-may-2016-1-2pm-lh101">Monday, 23 May, 2016, 1-2PM, LH101</h3>
<p>Cancelled.</p>
<h3 id="monday-16-may-2016-1-2pm-lh101">Monday, 16 May, 2016, 1-2PM, LH101</h3>
<ul>
<li>Reading: "A Non-Type-Theoretic Definition of Martin-Löf's Types" by Stuart Allen. Available from <a href="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/lics87.html">Cornell</a>. We should read <a href="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Allen/TR87-832-RESET.ps">the "Reset for better legibility" version of the tech report</a>.</li>
<li>Presenting: Tori Lewis</li>
</ul>
<h2 id="spring-2016">Spring 2016</h2>
<h3 id="monday-9-may-2016-1-2pm-lindley-hall-101">Monday, 9 May, 2016, 1-2PM, Lindley Hall 101</h3>
<ul>
<li>Reading: "Constructive Mathematics and Computer Programming" by Per Martin-Löf. A high-quality reprint of it is available from <a href="http://rsta.royalsocietypublishing.org/content/312/1522/501">The Royal Society</a> (works on-campus, at least).</li>
<li>Presenting: Dan Friedman</li>
</ul>
<h3 id="monday-2-may-2016-1-2pm-swain-west-217">Monday, 2 May, 2016, 1-2PM, Swain West 217</h3>
<ul>
<li>Reading: "On Sense and Reference" by Gottlob Frege. Jason got a copy through ILL and put it <a href="papers/on-sense-and-nominatum.pdf">here</a>.</li>
<li>Presenting: Jason Hemann</li>
</ul>
<h3 id="monday-25-april-2016-1-2pm-swain-west-217">Monday, 25 April, 2016, 1-2PM, Swain West 217</h3>
<ul>
<li>Reading: "Program Testing and The Meaning Explanations of Martin-Löf Type Theory" by Peter Dybjer. Chapter 11 of Epistemology versus Ontology, Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, 2012. Available from <a href="http://www.cse.chalmers.se/~peterd/papers/MartinLofFestschrift.pdf">the author's Web site</a> and, on campus, through <a href="http://link.springer.com/chapter/10.1007/978-94-007-4435-6_11">SpringerLink</a>.</li>
<li>Presenting: David Christiansen</li>
</ul>
<h3 id="monday-18-april-2016-1-2pm-swain-west-217.">Monday, 18 April, 2016, 1-2PM, Swain West 217.</h3>
<ul>
<li>Reading: "Intuitionistic Type Theory" (the Bibliopolis book) by Per Martin-Löf. Available online <a href="https://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf">from Johan Granström's page</a>.</li>
<li>Presenting: David Christiansen</li>
</ul>
<h1 id="topics">Topics</h1>
<h2 id="history-philosophy">History & Philosophy</h2>
<h3 id="background">Background</h3>
<ul>
<li>Gottlob Frege. On Sense and Reference (Über Sinn und Bedeutung)</li>
<li>Dana Scott. Constructive Validity. In Symposium on Automatic Demonstration, Volume 125 of the series Lecture Notes in Mathematics, pp. 237-275. Springer.</li>
</ul>
<h3 id="per-martin-löfs-writings">Per Martin-Löf's writings</h3>
<ul>
<li>An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North Holland, 1975.</li>
<li>Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, 1979. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982.</li>
<li>Intuitionistic type theory (the Bibliopolis book)</li>
<li>On the Meanings of the Logical Constants and the Justification of Logical Laws (lecture notes from 1983, printed in Nordic Journal of Philosophical Logic in 1996)</li>
<li>Truth of a proposition, evidence of a judgement, validity of a proof. Synthese 73(3), pp. 407--420. 1987.</li>
</ul>
<h3 id="further-developments">Further Developments</h3>
<ul>
<li>Hofmann and Streicher. The Groupoid Interpretation of Type Theory. (in "25 Years of Constructive Type Theory" or available from Streicher's Web page)</li>
</ul>
<h2 id="datatypes">Datatypes</h2>
<ul>
<li>Mendler, Nax. Inductive Definition in Type Theory. PhD thesis, Cornell, 1988.</li>
<li>Peter Dybjer. Inductive Families, in Formal Aspects of Computing 6, 1994</li>
<li>Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory, Journal of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525-549</li>
<li>Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. Pages 129 - 146 in Proceedings of TLCA 1999, LNCS 1581.</li>
<li>James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris. The Gentle Art of Levitation. ICFP 2010.</li>
</ul>
<h2 id="coinduction">Coinduction</h2>
<ul>
<li>Guarded Dependent Type Theory with Coinductive Types by Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal.</li>
<li>Guarded Cubical Type Theory: Path Equality for Guarded Recursion by Lars Birkedal, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi <a href="https://arxiv.org/pdf/1606.05223.pdf" class="uri">https://arxiv.org/pdf/1606.05223.pdf</a></li>
<li>Non-wellfounded trees in Homotopy Type Theory by Benedikt Ahrens, Paolo Capriotti, Régis Spadotti <a href="https://arxiv.org/pdf/1504.02949.pdf" class="uri">https://arxiv.org/pdf/1504.02949.pdf</a></li>
</ul>
<h2 id="meaning-explanations">Meaning Explanations</h2>
<ul>
<li>Peter Dybjer. Program Testing and The Meaning Explanations of Martin-Löf Type Theory. Epistemology versus Ontology, Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, 2012.</li>
<li>Anton Setzer: Coalgebras as Types determined by their Elimination Rules (in same book)</li>
</ul>
<h2 id="description-techniques">Description Techniques</h2>
<ul>
<li>N. G. de Bruijn. Telescopic Mappings in Typed Lambda Calculus. Information and Computation 91, pp. 189--204 (1991).</li>
</ul>
<h2 id="implementation-techniques">Implementation Techniques</h2>
<ul>
<li>Robert Harper and Robert Pollack. Type Checking with Universes.</li>
<li>Pattern Matching with Dependent Types. Thierry Coquand, Proc. of 1992 Workshop on Types for Proofs and Programs in Båstad.</li>
<li>Pattern Matching Without K. Jesper Cockx, Dominique Devriese, and Frank Piessens. Proceedings of ICFP 2014.</li>
</ul>
<h2 id="implementations">Implementations</h2>
<h3 id="coq"><span class="todo TODO">TODO</span> Coq</h3>
<h3 id="agda"><span class="todo TODO">TODO</span> Agda</h3>
<h3 id="idris">Idris</h3>
<ul>
<li>Edwin Brady. Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. JFP, October 2013.</li>
</ul>
<h3 id="nuprl">Nuprl</h3>
<ul>
<li>Robert Constable. Naive Computational Type Theory. Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259.</li>
</ul>
<h3 id="metaprl">MetaPRL</h3>
<ul>
<li>Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL - A Modular Logical Environment. TPHOLS 2003.</li>
</ul>
<h3 id="epigram">Epigram</h3>
<ul>
<li>The View From the Left (initial version)</li>
<li>The View From the Left (published version)</li>
</ul>
<h3 id="lego"><span class="todo TODO">TODO</span> LEGO</h3>
<h2 id="alternatives">Alternatives</h2>
<h3 id="calculus-of-inductive-constructions">Calculus of (Inductive) Constructions</h3>
<h3 id="observational-type-theory">Observational Type Theory</h3>
<ul>
<li>Thorsten Altenkirch and Conor McBride and Wouter Swierstra. Observational Equality, Now!. PLPV 2007.</li>
</ul>
<h3 id="zombie-trellys">Zombie Trellys</h3>
<ul>
<li>Casinghino, Sjöberg, and Weirich. Combining Proofs and Programs in a Dependently Typed Language. POPL '14.</li>
</ul>
<h3 id="homotopy-type-theory">Homotopy Type Theory</h3>
<ul>
<li><a href="https://arxiv.org/abs/1707.03693">Univalent Higher Categories via Complete Semi-Segal Types</a></li>
</ul>
<h3 id="cubical-type-theory">Cubical Type Theory</h3>
<ul>
<li>CCHM
<ul>
<li><a href="https://arxiv.org/abs/1611.02108">Cubical Type Theory: a constructive interpretation of the univalence axiom</a></li>
<li><a href="http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf">Axioms for Modelling Cubical Type Theory in a Topos</a></li>
</ul></li>
<li>CHiTT
<ul>
<li><a href="https://arxiv.org/abs/1712.01800">Computational Higher Type Theory III: Univalent Universes and Exact Equality</a></li>
<li><a href="https://arxiv.org/abs/1606.09638">Computational Higher Type Theory II: Dependent Cubical Realizability</a></li>
<li><a href="https://arxiv.org/abs/1604.08873">Computational Higher Type Theory I: Abstract Cubical Realizability</a></li>
</ul></li>
<li>Guarded Cubical
<ul>
<li><a href="https://arxiv.org/abs/1606.05223">Guarded Cubical Type Theory: Path Equality for Guarded Recursion</a></li>
</ul></li>
</ul>
<h2 id="find-the-right-papers-for-these"><span class="todo TODO">TODO</span> Find the right papers for these</h2>
<ul>
<li>Higher order unification - implementation</li>
</ul>
</body>
</html>