Seeking info on LM3 and Modula-3 compiler(s) (for PC if possible)

Dear Dr. Horning,
	You are listed in the book "Larch:  Languages and Tools for 
Formal Specification" as the source of information on LM3.  I am a 
mathematical software consultant (in the Boston area) with an interest in 
formal verification of programs.  I used to be an avid Pascal programmer, 
but due to marketplace demands, now do most of my work in C++.  I have 
not used Modula-3, but would be interested in starting to do so.  I am 
also interested in using the Larch system in conjunction with such work.
Would it be possible for you to answer the following questions?

	1)  What compilers are available for Modula-3?  What platforms do
	they run on?  Is it possible to find a compiler which runs on a
	PC?  More than one?  Under what operating system(s)?

	2)  Do I need to run under Unix to use the Larch system?  What about
	"Linux"?  What language is LM3 written in?  If it doesn't run on a
	PC, could it be ported?  What about other Larch tools?

Thank you kindly for your information.

John J. Rood