[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Hongwei Xi]

Hi,

After reading the messages on the issue of adequacy of representation,
I would like to point out that for a system like ATS/LF, the justification
for adequacy (when HOAS is involved) only relies on the strong 
normalization and Church-Rosser properties of the simply typed lambda 
calculus. This is due to a strict  separation between type indexes (static 
terms) and proofs (dynamic terms), which makes it possible to have

1) a "weak" language for type indexes
2) a "strong" language for proofs

To show that the proof language is indeed strong, we recently finished in
ATS/LF a direct encoding of Girard's proof of System F being strongly 
normalizing. 

More information on ATS/LF is available at:

http://www.cs.bu.edu/~hwxi/ATS/ATS.html

So the point here is that separation between types and proofs can make it 
a lot easier to justify adequacy of representation while also supporting a 
powerful proof language.

Cheers,

--Hongwei Xi

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi at cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)