Skip to content

Commit 933ecfa

Browse files
committed
Update about and bib
1 parent 55ba6d9 commit 933ecfa

File tree

2 files changed

+14
-19
lines changed

2 files changed

+14
-19
lines changed

_bibliography/papers.bib

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,4 +87,15 @@ @inproceedings{AbreuDHJMS23
8787
preview={coq.png}
8888
}
8989

90+
@inproceedings{AbreuBCDHJMS23,
91+
author = {Pedro Abreu and Sage Binder and Anthony Cantor Benjamin Delaware and Alex Hubers and Christa
92+
Jenkins and J. Garrett Morris and Aaron Stump},
93+
title = {A Type-Based Approach to Divide-and-Conquer Recursion in Coq},
94+
booktitle = {Journal of Functional Programming},
95+
year = 2025,
96+
doi = {},
97+
url = {},
98+
preview={coq.png}
99+
}
100+
90101

_pages/about.md

Lines changed: 3 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -20,22 +20,6 @@ social: true # includes social icons at the bottom of the page
2020

2121

2222
I am a doctoral candidate in Computer Science at the University of Iowa, where I'm a
23-
member of the [Computational Logic Center](https://clc.cs.uiowa.edu/site/). I
24-
like (functional) programming languages, semantics, and type theory.
25-
26-
27-
My active research interest is in expressing [extensible data
28-
types](https://arxiv.org/abs/2307.08759) using [row
29-
types](https://dl.acm.org/doi/10.1145/3290325) (with Dr. J. Garrett Morris,
30-
Co-Advisor). My current work is in expanding the expressivity of
31-
[System Rω](https://arxiv.org/abs/2307.08759), a higher-order row calculus with
32-
label-generic combinators.
33-
34-
I am also very interested in:
35-
36-
- various applications of row type systems, e.g. [session types](https://homepages.inf.ed.ac.uk/slindley/papers/fst-extended.pdf), and [algebraic effects & handlers](https://dl.acm.org/doi/10.1145/2976022.2976033);
37-
- language mechanization in Agda, by way of both [shallow
38-
embeddings](https://github.com/IaFP/ROmega-ICFP23) (with denotational semantics)
39-
and [deep embeddings](https://github.com/IaFP/System-F-to-R-Omega/) (with operational semantics);
40-
- and using [Mendler-style recursion schemes](https://github.com/astump/dc-recursion-examples) to enforce *type-based* termination checking in total languages (e.g. [Coq](https://dl.acm.org/doi/10.1145/3571196)).
41-
23+
member of the [Computational Logic Center](https://clc.cs.uiowa.edu/site/), advised by Dr. [J. Garrett Morris](https://jgbm.github.io/).
24+
I like programming languages, type theory, and language mechanization.
25+
My active research interest is in mechanizing row type theories in Agda. I will tentatively graduate in the Fall of 2025 and will be focusing my job search to (i) teaching focused jobs at SLACs (small/selective liberal arts colleges) in the US and (ii) post-doctoral positions in the UK & Europe.

0 commit comments

Comments
 (0)