## Welcome!

I am a third-year PhD student in the Department of Computer Science and Engineering at the University of Michigan. My advisor is Professor Max New. In May 2021, I obtained my MSE in Computer and Information Science from the University of Pennsylvania. During my time at Penn, I was fortunate to work with Professor Stephanie Weirich on the hs-to-coq tool as part of an independent study. Previously, I attended Rutgers University New Brunswick, where I studied Computer Science and Math.

My research interests are primarily in the theoretical study of programming languages. I am especially interested in applying tools from mathematics (e.g., category theory) to build and analyze programming languages. More broadly, I am also interested in theoretical areas of computer science as a whole, including Theory A topics (e.g., computational complexity theory).

**email**: ericgio AT umich DOT edu

### News

- October 2023: Attending SPLASH 2023 in Portugal to present our paper "Gradual Typing for Effect Handlers".
- September 2023: Officially achieved PhD candidacy!
- August 2023: Our paper "Gradual Typing for Effect Handlers" has been accepted to OOPSLA 2023!
- June 2023: Attending PLDI 2023 virtually as a student volunteer.
- May 2023: Passed my CSE Prelim Exam!
- August 2021: Started PhD in CSE at University of Michigan.
- June 2021: Attended OPLSS 2021.
- May 2021: Graduated from Penn.
- April 2021: I have selected a PhD program! I will be attending the University of Michigan beginning fall 2021.
- December 2020: Gave a presentation to the Penn PLClub.
- August 2020: Attended PLMW at ICFP 2020. My first PLMW and first conference.

### Research Projects

- Mechanized Metatheory for Gradually-Typed Languages Via Synthetic Guarded Domain Theory
- Gradual Typing for Effect Handlers: I contributed to proving metatheoretic properties of GrEff, a proof-of-concept gradually-typed programming language with effects. The language is designed to model the situation where one would like to retrofit an effect typing system onto an existing programming language with effects.
- Invariants with
`hs-to-coq`

(Jan 2020-Sept 2020): I worked on modifying the`hs-to-coq`

tool to support automatically generating proof obligations for datatype invariants.

### Talks and Presentations

- Datatype invariants with
`hs-to-coq`

(talk given at Penn's PLClub)
- Comparing monad transformers and algebraic effects in Haskell

### Service

- [October 2023] SPLASH 2023: Student volunteer
- [October 2023] Midwest PL Summit 2023: Student volunteer
- [June 2023] PLDI 2023: Student volunteer (virtual)
- [April 2023] Faculty candidate graduate student host
- [Fall 2022 - Winter 2023] MPLSE Reading group organizer