-
Notifications
You must be signed in to change notification settings - Fork 0
/
articles.html
79 lines (53 loc) · 2.99 KB
/
articles.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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<head>
<link rel="stylesheet" href="css/style.css" type="text/css"/>
<meta http-equiv="Content-Type" content="text/html; charset=utf8">
<title>LMFI: Théorie des types homotopiques (liste d'articles)</title>
</head>
<body>
<h4>Articles historiques</h4>
<ul>
<li>Herman Geuvers, <a href="https://pure.tue.nl/ws/files/2181809/9511424.pdf">A short and flexible proof of strong normalization for the
calculus of constructions</a>, 1994.
</li>
<li>Per Martin-Löf, <a href="http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf">An intuitionistic theory of types</a>, 1973.</li>
<li>Peter Dybjer, <a
href="http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf">Inductive
families</a>, 1997.
</li>
</ul>
<h4>Articles spécifiquement sur la théorie des types homotopique</h4>
<ul>
<li>Daniel R. Licata, Guillaume Brunerie, <a
href="http://dlicata.web.wesleyan.edu/pubs/lb13cpp/lb13cpp.pdf">π<sub>n</sub>(S<sup>n</sup>)
in Homotopy Type Theory</a>, 2013.
</li>
<li>Marc Lasson, <a
href="https://ac.els-cdn.com/S1571066114000802/1-s2.0-S1571066114000802-main.pdf?_tid=00622de3-d1d3-46cc-951c-ea425c248fb4&acdnat=1520263067_4301b864ba1cfa47a6a80eb7d17b203e">Canonicity
of Weak ω-groupoid Laws Using Parametricity Theory</a>, 2014.
</li>
<li>Carlo Angiuli, Ed Morehouse, Daniel R. Licata, Robert Harper <a href="https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf">Homotopical Patch Theory</a>, 2014.</li>
<li>Hugo Herbelin, <a href="http://pauillac.inria.fr/~herbelin/articles/mscs-Her14-semisimplicial.pdf">A dependently-typed construction of semi-simplicial types</a>, 2015.</li>
<li>Ambrus Kaposi, András Kovács, Thorsten Altenkirch, <a href="https://akaposi.github.io/finitaryqiit.pdf">Constructing Quotient Inductive-Inductive Types</a>, 2019.</li>
<li>Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg, <a href="https://arxiv.org/pdf/1611.02108.pdf">Cubical Type Theory: a constructive interpretation of the univalence axiom</a> (sections 1 à 4), 2015.</li>
</ul>
<h4>Articles développant de nouveaux formalismes ou nouvelles traductions</h4>
<ul>
<li>Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu
Sozeau, Nicolas Tabareau, <a
href="https://hal.inria.fr/hal-01319066"> The Definitional Side of
the Forcing</a>, 2016.
</li>
<li>Olivier Laurent, <a href="https://perso.ens-lyon.fr/olivier.laurent/idn.pdf">Intuitionistic Dual-intuitionistic Nets</a>
2005.
</li>
<li>Paul Blain Levy, <a href="http://www.cs.bham.ac.uk/~pbl/papers/hosc04.pdf">
Call-By-Push-Value: Decomposing Call-By-Value And Call-By-Name</a>,
2005.
<li>Paul-André Melliès, Nicolas Tabareau, <a href="https://www.irif.fr/~mellies/papers/resource-modalities-apal.pdf">Resource modalities in tensor logic</a>,
2010.</li>
<li>Pierre-Marie Pédrot, Nicolas Tabareau, <a href="https://www.pédrot.fr/articles/exceptional.pdf">Failure is Not an Option - An Exceptional Type Theory</a>, 2018.</li>
</ul>
</body>
</HTML>