The semantics of reflected proof, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp.95-197, 1990. ,
Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.57-68, 2007. ,
DOI : 10.1145/1292597.1292608
Lambda Calculi with Types, Handbook of Logic in Computer Science, 1992. ,
The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the, 1984. ,
Implementing Reflection in Nuprl, 2006. ,
Using Reflection to Explain and Enhance Type Theory, Proof and Computation, pp.65-100, 1994. ,
DOI : 10.1007/978-3-642-79361-5_3
Inductively defined types, COLOG-88, pp.50-66, 1990. ,
DOI : 10.1007/3-540-52335-9_47
On the expressive power of programming languages, Science of Computer Programming, pp.134-151, 1990. ,
Proofs and types, 1989. ,
Programming in Martin- Löf 's Type Theory: An Introduction, 1990. ,
Inductively defined types in the Calculus of Constructions, Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, pp.209-228, 1990. ,
DOI : 10.1007/BFb0040259
Types and programming languages, 2002. ,
Strong normalization for non-structural subtyping via saturated sets, Information Processing Letters, vol.58, issue.4, pp.157-162, 1996. ,
DOI : 10.1016/0020-0190(96)00056-7
Truth and internalizability. Draft available from http://people. cohums.ohio-state, p.1, 2010. ,
Equality, Quasi-Implicit Products, and Large Eliminations, Workshop on Intersection Types and Related Systems (ITRS), 2010. ,
DOI : 10.4204/EPTCS.45.7
Investigations into Intensional Type Theory, 1993. ,
Aura: Programming with Authorization and Audit, 2009. ,
Take arbitrary u ? [[S 1 ]] ? . By definition, we know (t u) ? [, With our reduction strategy, (t u) ? (t ? u). By IH(CR 2) ,
By definition, we know (t ? u) ? [ With our reduction strategy By IH(CR 1), u is closed, thus we know (t u) is closed, By IH(CR, vol.3, issue.1 ,
We know that ? is non-empty (for example, V ? ?) Take an arbitrary reducibility candidate R. By definition of, By IH(CR 1), t ? V ,
Consider arbitrary reducibility candidate R. By definition, t ?, By IH, issue.2 ,
Take arbitrary reducibility candidate R. By definition, t ? ? We know that t ? t ? and t is closed ,