From 88a47f00de192f74acd3eb0985be29362f8bec06 Mon Sep 17 00:00:00 2001 From: lkuper Date: Wed, 10 Jan 2024 21:37:30 +0000 Subject: [PATCH] regenerate after: Merge branch 'main' of github.com:lsd-ucsc/lsd-ucsc.github.io --- index.xml | 8 ++++---- lsd-seminar/2024wi/index.html | 8 ++++---- themes/academic | 1 - 3 files changed, 8 insertions(+), 9 deletions(-) delete mode 160000 themes/academic diff --git a/index.xml b/index.xml index 076fe77..43df780 100644 --- a/index.xml +++ b/index.xml @@ -48,7 +48,7 @@ <tr> <td><a href="#jan-19">Jan. 19</a></td> <td>Katherine Philip</td> -<td><em>TBD</em></td> +<td>Formalizing Type-Directed Specialization</td> </tr> <tr> @@ -123,11 +123,11 @@ <p><strong>Speaker:</strong> Katherine Philip</p> -<p><strong>Title:</strong> <em>TBD</em></p> +<p><strong>Title:</strong> Formalizing Type-Directed Specialization</p> -<p><strong>Abstract:</strong> <em>TBD</em></p> +<p><strong>Abstract:</strong> We present a formal study of type-directed specialization, an implementation and optimization technique for implementing parametric polymorphism in programming languages. Type-directed specialization (also known as monomorphization) systematically eliminates polymorphic code by generating monomorphic copies, each specialized for a particular type. We focus on the full specialization of parametric polymorphic expressions in an ML-like language that uses the Hindley-Milner type system. We formalize this with a family of representation transformation functions that translate source language programs into a novel target language that is capable of binding the potentially infinite families of specialized functions generated by full specialization. A key contribution of this paper is to prove that these functions preserve typing for all well-typed source programs. Finally, we lay the groundwork for future study of semantics preservation and for the formalization of other kinds of specialization and representation transformations.</p> -<p><strong>Bio:</strong> <em>TBD</em></p> +<p><strong>Bio:</strong> Katherine is a PhD student at Portland State University, advised by Mark P. Jones. They are interested in the design and implementation of efficient languages for low-level systems development. Currently, they are working on the Habit programming language (<a href="https://www.habit-lang.org/" rel="noreferrer" target="_blank">https://www.habit-lang.org/</a>).</p> <h1 id="jan-26">Jan. 26</h1> diff --git a/lsd-seminar/2024wi/index.html b/lsd-seminar/2024wi/index.html index d40e7f9..2215bf3 100644 --- a/lsd-seminar/2024wi/index.html +++ b/lsd-seminar/2024wi/index.html @@ -229,7 +229,7 @@

Languages, Systems, and Data Seminar (Winter 2024)

Jan. 19 Katherine Philip -TBD +Formalizing Type-Directed Specialization @@ -304,11 +304,11 @@

Jan. 19

Speaker: Katherine Philip

-

Title: TBD

+

Title: Formalizing Type-Directed Specialization

-

Abstract: TBD

+

Abstract: We present a formal study of type-directed specialization, an implementation and optimization technique for implementing parametric polymorphism in programming languages. Type-directed specialization (also known as monomorphization) systematically eliminates polymorphic code by generating monomorphic copies, each specialized for a particular type. We focus on the full specialization of parametric polymorphic expressions in an ML-like language that uses the Hindley-Milner type system. We formalize this with a family of representation transformation functions that translate source language programs into a novel target language that is capable of binding the potentially infinite families of specialized functions generated by full specialization. A key contribution of this paper is to prove that these functions preserve typing for all well-typed source programs. Finally, we lay the groundwork for future study of semantics preservation and for the formalization of other kinds of specialization and representation transformations.

-

Bio: TBD

+

Bio: Katherine is a PhD student at Portland State University, advised by Mark P. Jones. They are interested in the design and implementation of efficient languages for low-level systems development. Currently, they are working on the Habit programming language (https://www.habit-lang.org/).

Jan. 26

diff --git a/themes/academic b/themes/academic deleted file mode 160000 index 8d596ff..0000000 --- a/themes/academic +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 8d596ffed2d080010c561679cf4e9b4da1554781