-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
82 lines (82 loc) · 5.09 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
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<meta name="author" content="Paolo G. Giarrusso" />
<title>Incremental λ-Calculus</title>
<style>
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
</style>
<link rel="stylesheet" href="ilc.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 id="title-block-header">
<h1 class="title">Incremental λ-Calculus</h1>
<p class="author">Paolo G. Giarrusso</p>
</header>
<h1 id="introduction">Introduction</h1>
<p>This is the homepage for the <strong>Incremental λ-Calculus</strong> project. Our goal is to extend database technology for low-overhead incremental computation, based on finite differencing, and apply it to higher-order languages.</p>
<h1 id="publications">Publications</h1>
<ul class="incremental">
<li><a href="https://link.springer.com/chapter/10.1007/978-3-030-17184-1_20">Incremental λ-Calculus in Cache-Transfer Style — Static Memoization by Program Transformation</a>. Paolo G. Giarrusso, Yann Régis-Gianas and Philipp Schuster. ESOP 2019. Supersedes Chapter 17 of Giarrusso’s PhD thesis.
<ul class="incremental">
<li><a href="https://github.com/yurug/cts/blob/ae1bf7b4b7ef82167324c7ce18dc3785b7dcaab7/static-caching-extended.pdf">Extended version</a>.</li>
<li>Supplementary material: <a href="https://github.com/yurug/cts">Implementation and Coq formalization</a>.</li>
</ul></li>
<li><a href="resources/pldi14-ilc-author-final.pdf">A theory of changes for higher-order languages — incrementalizing λ-calculi by static differentiation</a> (updated version). Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel and Klaus Ostermann. PLDI 2014, pp. 145–155.
<ul class="incremental">
<li><a href="https://github.com/inc-lc/ilc-scala">Scala prototype — inc-lc/ilc-scala</a></li>
<li><a href="https://github.com/inc-lc/ilc-agda">Agda machine-checked proofs — inc-lc/ilc-agda</a>.</li>
</ul></li>
<li><a href="resources/giarrusso-phd-thesis-2020-final.pdf">Optimizing and Incrementalizing Higher-order Collection Queries by AST Transformation</a>. Paolo G. Giarrusso’s PhD thesis. Some highlights:
<ul class="incremental">
<li>A novel, simpler correctness proof for ILC on simply-typed λ-calculus, where validity is captured by a logical relation (Ch. 12-13-14).</li>
<li>A reformulation of that proof using (step-indexed) logical relations and operational semantics, for simply-typed λ-calculus (without or with recursion) and untyped λ-calculus (Appendix C).</li>
<li>Chapter 17 is superseded by the extended version of the ESOP’19 paper.</li>
<li><a href="https://github.com/inc-lc/ilc-agda/tree/master/Thesis/">Agda machine-checked proofs — inc-lc/ilc-agda/Thesis</a>, for Ch. 12-14.</li>
</ul></li>
</ul>
<h1 id="related-papers">Related papers</h1>
<p>By other authors:</p>
<ul class="incremental">
<li><a href="https://dl.acm.org/doi/abs/10.1145/3371090">Seminaïve evaluation for a higher-order functional language</a>. Michael Arntzenius and Neel Krishnaswami. POPL 2020.</li>
</ul>
<h1 id="credits">Credits</h1>
<p>This project benefited from code and ideas of many different people:</p>
<ul class="incremental">
<li>Cai Yufei</li>
<li>Paolo G. Giarrusso</li>
<li>Tillmann Rendel</li>
<li>Klaus Ostermann</li>
<li>Lourdes Del Carmen Gonzàlez Huesca</li>
<li>Yann Régis-Gianas</li>
<li>Philipp Schuster</li>
</ul>
<p>Further acknowledgments in each publication.</p>
<h1 id="news">News</h1>
<ul class="incremental">
<li>2020-01-23: Updated version of this page and of Giarrusso’s PhD thesis.</li>
<li>2015-03-16: <a href="resources/2015-01-22%20ILC%20Paris.pdf">Slides of the Paris talk online</a>.</li>
<li>2015-01-22: <a href="http://blaisorblade.github.io/blog/2015/01/15/a-talk-on-ilc/">Talk about ILC project at the Paris Diderot (Paris 7) University</a>.</li>
<li>2014-06-07: Sources online on GitHub — see <a href="https://github.com/inc-lc/ilc-scala">inc-lc/ilc-scala</a> and <a href="https://github.com/inc-lc/ilc-agda">inc-lc/ilc-agda</a>.</li>
<li>2014-05-04: Author’s version of the paper camera-ready finally online.</li>
<li>2014-03-15: The AEC submission was found to “meet or exceed expectations”!</li>
<li>2014-02-21: <a href="AEC.html">Link to the AEC submission</a>.</li>
<li>2014-02-10: Submission to the artifact evaluation committee (AEC) evaluation</li>
<li>2014-02-05: Website online</li>
<li>2014-02-03: Our first paper on this project was accepted for PLDI ’14! The author’s version of the camera-ready is available.</li>
</ul>
<h1 id="contacts">Contacts</h1>
<p>For any question or suggestion, feel free to contact me, Paolo G. Giarrusso, at p !dot! giarrusso (at) gmail !dot! com.</p>
</body>
</html>