Audrey Seo

Audrey Seo

4th year PhD student, studying programming languages.

Publications

Correctly Compiling Proofs About Programs Without Proving Compilers Correct

Published in Interactive Theorem Proving 2024, 2024

This paper explores a technique to get guarantees about compiled programs even in the presence of an unverified, or even incorrect, compiler. Our workflow compiles programs, specifications, and proof objects, from an embedded source language and logic to an embedded target language and logic. We implement two simple imperative languages, each with its own Hoare-style program logic, and a framework for instantiating proof compilers out of compilers between these two languages that fulfill certain equational conditions in Coq.

Recommended citation: Seo, Audrey, Lam, Chris, Grossman, Dan, and Ringer, Talia. (2024). "Correctly Compiling Proofs About Programs Without Proving Compilers Correct." Interactive Theorem Proving 2024. http://audreyseo.github.io/files/proof_compilers_itp_2024.pdf

Enhancing Abstraction in App Inventor with Generic Event Handlers

Published in IEEE Blocks and Beyond Workshop, 2019

This paper outlines improvements to the blocks programming language MIT App Inventor made based on observations from analyses of previous work.

Recommended citation (bib): Patton, Evan, Seo, Audrey, and Turbak, Franklyn. (2019). "Enhancing Abstraction in App Inventor with Generic Event Handlers." IEEE Blocks and Beyond Workshop. http://audreyseo.github.io/files/blocks_and_beyond.pdf

Abstractionless Programming in App Inventor

Published in ACM SPLASH BLOCKS+ Workshop, 2018

In this paper, an analysis shows that many of the opportunities for abstraction involve a difficult concept in App Inventor, generics. We make the hypothesis that this is the main reason for App Inventor programmers’ lack of abstractions, and recommend that more work be done to teach App Inventor programmers about generics.

Recommended citation (bib): Seo, Audrey. (2018). "Abstractionless Programming in App Inventor." ACM SPLASH BLOCKS+. http://audreyseo.github.io/files/blocksplus18-paper19.pdf