Dongho Lee

Research interests

In general, my research interest is to understand better the relationship between logic and computation. I like to think about the following three inspiring examples of such relation:

  • Curry-Howard correspondence between the intuitionistic logic and the lambda-calculus;
  • the adjointness of toposes and type theories; and
  • Fagin's characterization of the NP complexity class.

In the Friendly Logic course in 2017, Scott Weinstein and Val Tannen have pointed out that

"One of the fundamental insights of (mathematical) logic is that our understanding of (...) phenomena is enriched by elevating the languages we use to describe (...) structures to objects of explicit study."

To me, logic is about how we express the structures that we are interested in. Given that computation and its properties are expressed in different programming languages and type systems, it is not surprising that we have various connections between these languages and type systems and logic. Furthermore, we could describe the relations abstractly by using category theory.

At the same time, not all logics are the same in terms of expressivity and provability. Once we regard logic as a precise description of some structures, specific logic can help us understand the object. Conversely, the knowledge on the specific structure can help understand better the problems in logic. This is the reason why Fagin's characterization would be interesting for both those who are interested in complexity theory and those who want to understand the generalized spectra problem in logic.

It has been several years that I have been interested in quantum computation and wanted to understand what we can do with quantum computers. In order to do that, I would like to investigate logics related to quantum computation which express and characterize various effects and properties of quantum programs.

Research activities

As a project for an independent study, I studied finite model theory and theories of infinite strings with Scott Weinstein in 2017. The goal was to investigate the axiomatizability of the theories of infinite strings and find an axiomatization if possible using model theoretic approach. We did not reach to the initial goal but showed that the theory does not have the quantifier elimination property which means that there are some formulas with quantifier which have no equivalent quantifier-free formula.

I have been firstly introduced to quantum programming language QWire when I did an internship with Steve Zdancewic from 2017 fall to 2018 spring. I did a project on a compiler from QWire to quantum assembly language called QASM. I also participated in a paper on reversible quantum circuit where I implemented and verified a quantum adder in Coq by using the verified compiler of boolean expression proposed in the same paper.

In 2018, I have started my PhD with Benoît Valiron and Valentin Perrelle at the LMF (, which was the LRI at that time) and the CEA on the formal methods for quantum programming languages. We have designed a programming langue for quantum circuit description called Proto-Quipper-L with a linear/non-linear type system to formalize dynamic lifting in Quipper, and have given it an operational and a denotational semantics based on a concrete category. I am interested in adding quantifiers to the type systems and see if we can interpret in the concrete categorical model.

Publications

(Abstract submitted to a workshop) Dongho Lee, Sébastien Bardin, Valentin Perrelle and Benoît Valiron. Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control. Programming Languages for Quantum Computing (PLanQC’20).

(Co-authored paper) Robert Rand, Jennifer Paykin, Dong-Ho Lee and Steve Zdancewic. ReQWIRE: Reasoning about Reversible Quantum Circuits. International Conference on Quantum Physics and Logic (QPL’18).

(In progress) Dongho Lee, Valentin Perrelle and Benoît Valiron. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. Foundations of Software Technology and Theoretical Computer Science (FSTTCS'21).

Interests from other areas

I like listening to music and playing the piano and the cello. Some of my favorites are the recordings of Jacqueline du Pré and Yo-Yo Ma.

I enjoy watching movies online especially during the confinement.

I like talking with others and having beer events such as in the ones with QuaCS team.

I enjoy riding a bike and running.

I am also interested in some social problems like:

  • to build a voting system where the voters can program their votes;
  • to find a definition of job to ameliorate unemployment problem; and
  • to obtain international cooperation despite the presence of prisoners' dilemma.

Contact

Anybody who wants to talk about anything mentioned above, please contact through:

  • Email: fredldh (at) gmail (dot) com