Re: Subject reduction fails in Java

• To: gunter@saul.cis.upenn.edu
• Subject: Re: Subject reduction fails in Java
• From: Matthias Felleisen <matthias@cs.rice.edu>
• Date: Tue, 23 Jun 1998 08:09:45 -0500 (CDT)
• CC: types@cs.indiana.edu, mflatt@cs.rice.edu, shriram@cs.rice.edu
• Delivery-Date: Tue, 23 Jun 1998 09:11:07 -0500
• In-reply-to: <199806231253.IAA02353@saul.cis.upenn.edu> (message from Carl Gunter on Tue, 23 Jun 1998 08:53:13 -0400 (EDT))
• Reply-to: matthias@rice.edu

[This is a response to two people ...]

Carl, yes, I meant "models" of the languages Ml and Java in the sense of
physical models (ignore friction and let's study the rest). Apologies if 
this causes confusion, but the point of my message remains the same. 

Donald, the til & tal projects at Cornell and CMU use type information at
ALL stages of compilation/implementation. They are successful in exploiting
them. I don't think that this is an issue of theoreticians making strong
assumptions. Furthermore, it is perfectly okay to formulate models that are
good for one purpose (say, proving type soundness) and others that are good
for other purposes (say, proving a jvm implementation correct). If you do
so, you need to relate the models with (strong) adequacy theorems to ensure
that the two evaluation sequences ("executions") preserves the correct
"subject" so that your other theorems make sense. But that should be all. 

Regards -- Matthias 

• Re: Subject reduction fails in Java
• From: Carl Gunter <gunter@saul.cis.upenn.edu>

• Prev: CADE-15: Call for Attendance
• Next: Re: Subject reduction fails in Java
• Index(es):
  • Main
  • Thread