TY  - RPRT
TI  - Internalising modified realisability in constructive type theory
AU  - Erik Palmgren
PY  - 2005
DO  - 10.2168/lmcs-1(2:2)2005
UR  - https://arxiv.org/abs/math/0505418
ID  - math/0505418
ER  -