<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>5905</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR></AUTHORS><YEAR>2001</YEAR><TITLE>A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL</TITLE><PLACE_PUBLISHED>Theorem Proving in Higher Order Logics - Proceedings of the 14th International Conference, TPHOLs 2001 (R.J.Boulton and P.B.Jackson, eds). Volume 2152 of Lecture Notes in Computer Science, Springer-Verlag. DOI: 10.1007/3-540-44755-5_16</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>217-232</PAGES><ISBN>3-540-42525-X</ISBN><LABEL>Gay:2001:5905</LABEL><KEYWORDS><KEYWORD>types</KEYWORD></KEYWORDS<ABSTRACT>We present a formalisation, in the theorem proving system Isabelle/HOL, of a linear type system for the pi calculus, including a proof of runtime safety of typed processes. The use of a uniform encoding of pi calculus syntax in a meta language, the development of a general theory of type environments, and the structured formalisation of the main proofs, facilitate the adaptation of the Isabelle theories and proof scripts to variations on the language and other type systems.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/tphols2001.pdf</URL></RECORD></RECORDS></XML>