Collaborated with:M.Rapoport I.Kabir O.Lhoták L.Xia Yannick Zakowski C.Hur G.Malecha B.C.Pierce S.Zdancewic
Talks about:interact (1) program (1) repres (1) recurs (1) object (1) depend (1) sound (1) simpl (1) proof (1) impur (1)
Person: Paul He
DBLP: He:Paul
Contributed to:
2017
2020Wrote 2 papers:
- OOPSLA-2017-RapoportKHL #proving
- A simple soundness proof for dependent object types (MR, IK, PH, OL), p. 27.
- POPL-2020-XiaZHHMPZ #coq #interactive #recursion #representation #source code
- Interaction trees: representing recursive and impure programs in Coq (LyX, YZ, PH, CKH, GM, BCP, SZ), p. 32.