LARA MONA HOL Connecting MONA and HOL Relavant papers: Combining WS1S with HOL, from http://www.inf.ethz.ch/personal/basin/pubs/pubs.html Integrating WS1S with PVS, from http://www.csl.sri.com/users/owre/papers/cav00/index.html SAV08 lectures Lecture22 Lecture23