[POPLmark] (no subject)

[danwang at CS.Princeton.EDU]

Just curious if the POPLmark authors were aware of the following approach?

http://www.cs.le.ac.uk/pac/Themes/HOASIC.html

@INPROCEEDINGS{ACMchoasttpci,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  TITLE = {{Combining Higher Order Abstract Syntax with Tactical Theorem   
Proving and (Co)Induction}},
  BOOKTITLE = {Proceedings of the 15th International Conference on 
             Theorem Proving in Higher Order Logics, Hampton, VA, USA},
  YEAR = {2002},
  PAGES = {13--30},
  PUBLISHER = {Springer-Verlag},
  VOLUME = {2410},
  SERIES = {Lecture Notes in Computer Science},
  HTTP = {http://www.mcs.le.ac.uk/~rcrole/papers/choasttpci.ps.gz}
}

I didn't notice it in the POPLMARK paper, and it seems like a promissing 
approach.


-------------------------------------------------
This mail sent through IMP: http://horde.org/imp/