Collaborated with:Fabian Kunze Marc Roth M.Sozeau Simon Boulier N.Tabareau Théo Winterhalter
Talks about:coq (4) calculus (1) correct (1) reason (1) erasur (1) verif (1) space (1) check (1) weak (1) valu (1)
Person: Yannick Forster 0002
DBLP: 0002:Yannick_Forster
Contributed to:
2020Wrote 2 papers:
- POPL-2020-ForsterKR #call-by #λ-calculus
- The weak call-by-value λ-calculus is reasonable for both time and space (YF0, FK, MR), p. 23.
- POPL-2020-SozeauBFTW #coq #exclamation #type checking #verification
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.