Papers

These are most of my papers that are available online. I'm not currently maintaining this list, so the more recent stuff will need to be found elsewhere.

Ian A. Mason.
The Metatheory of the Classical Propositional Calculus is not Axiomatizable.
Journal of Symbolic Logic., 50(2):451-457, June 1985.
[ps, pdf].

Ian A. Mason.
Hoare's Logic in the LF.
Technical Report ECS-LFCS-87-32, Laboratory for Foundations of Computer Science, University of Edinburgh, 1987.
Available as postscript from [ps, pdf].

A.Avron, F.Honsell, and Ian A. Mason.
An Overview of the Edinburgh Logical Framework.
In G.Birtwistle and P.A.Subramanyam, editors, Current Trends in Hardware Verifications and Automated Theorem Proving. Springer-Verlag, 1989.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Axiomatizing Operational Equivalence in the Presence of Side Effects.
In Fourth Annual Symposium on Logic in Computer Science, pages 284-293. IEEE, 1989.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Programming, Transforming, and Proving with Function Abstractions and Memories.
In Proceedings of the 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa, volume 372 of Lecture Notes in Computer Science, pages 574-588. Springer-Verlag, 1989.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
A Sound and Complete Axiomatization of Operational Equivalence Between Programs with Memory.
Technical Report STAN-CS-89-1250, Department of Computer Science, Stanford University, 1989.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Reasoning About Programs with Effects.
In Programming Language Implementation and Logic Programming, PLILP'90, volume 456 of Lecture Notes in Computer Science, pages 189-203. Springer-Verlag, 1990.
[ps, pdf].

Ian A. Mason, J.Pehoushek, Carolyn L. Talcott, and J.Weening.
Programming in QLisp.
Technical Report STAN-CS-90-1340, Department of Computer Science, Stanford University, 1990.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Program Transformation for Configuring Components.
In Proceedings of the ACM/IFIP Symposium on Partial Evaluation and Semantics Based Program Manipulation., pages 297-308, 1991.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Equivalence in Functional Languages with Effects.
Journal of Functional Programming, 1:287-327, 1991.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Inferring the Equivalence of Functional Programs that Mutate Data.
Theoretical Computer Science, 105(2):167-215, 1992.
[ps, pdf].

Arnon Avron, Furio Honsell, Ian A. Mason, and Robert Pollack.
Using Typed Lambda Calculus to Implement Formal Systems on a Machine.
Journal of Automated Reasoning, 9:309-354, 1992.
[ps, pdf].

Furio Honsell, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott.
A Variable Typed Logic of Effects.
Information and Computation, 119(1):55-90, May 1995.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
References, Local Variables and Operational Reasoning.
In Sixth Annual Symposium on Logic in Computer Science, pages 186-197. IEEE, 1991.
[ps, pdf].

Gul Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott.
Towards a theory of Actor Computation.
In Concur '92, volume 630 of Lecture Notes in Computer Science, pages 565-579. Springer-Verlag, 1992.
[ps, pdf].

Saša Buvac and Ian A. Mason.
Propositional Logic of Context.
In Proceedings of Eleventh Annual National Conference on Artificial Intelligence AAAI'93, pages 412-419. AAAI Press/ MIT Press, 1993.
[ps, pdf].

Saša Buvac, Vanja Buvac, and Ian A. Mason.
The Semantics of Propositional Contexts.
In Proceedings of the Eight International Symposium on Methodologies for Intelligent Systems, volume 869 of Lecture Notes in Artificial Intelligence. Springer Verlag, 1994.
[ps, pdf].

Furio Honsell, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott.
A Theory of Classes for a Functional Language with Effects.
In E. Börger, G.Jäger, H.Kleine Büning, S.Martini, and M.M. Richter, editors, Computer Science Logic, Selected papers from CSL'92, volume 702 of Lecture Notes in Computer Science, pages 309-326. Springer, Berlin, 1993.
[ps, pdf].

Gul Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott.
A Foundation for Actor Computation.
Journal of Functional Programming, 7:1-72, 1997.
[ps, pdf].

Saša Buvac, Vanja Buvac, and Ian A. Mason.
Metamathematics of Contexts.
Fundamenta Informaticae, 23(3), 1995.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Program Transformation via Contextual Assertions.
In Logic, Language and Computation. Festschrift in Honor of Satoru Takasu, volume 792 of Lecture Notes in Computer Science, pages 225-254. Springer, Berlin, 1994.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Reasoning about Object Systems in VTLoE.
International Journal of Foundations on Computer Science, 6(3):265-298, 1995.
[ps, pdf].

Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott.
From Operational Semantics to Domain Theory.
Information and Computation, 128(1):26-47, 10 1996.
[ps, pdf].

Jacob Frost and Ian A. Mason.
An Operational Logic of Effects.
In Proceedings of the Australasian Theory Symposium, CATS '96, pages 147-156, 1996.
[ps, pdf].

Ian A. Mason.
A First Order Logic of Effects.
Theoretical Computer Science, pages 277 - 318, 1997.
[ps, pdf].

Ian A. Mason.
Parametric Computation.
In James Harland, editor, Proceedings of the Australasian Theory Symposium, CATS '97, pages 103 - 112, 1997.
[ps, pdf]. Complete proofs: [ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Actor Languages - Their Syntax, Semantics, Translation & Equivalence.
Theoretical Computer Science, 220:409-467, 1999.
[ps, pdf].

Ian A. Mason.
Computing with Contexts.
Higher-Order and Symbolic Computation, 12:171-201, 1999.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Feferman-Landin Logic.
In to appear in Reflections - A symposium hounoring Solomon Feferman on his 70th birthday, Lecture Notes in Logic. Association of Symbolic Logic, 2000.
[ps, pdf].

Ian A. Mason and Carolyn L. Talcott.
Simple Network Protocol Simulation within Maude.
In Shusaku Iida, editor, International Workshop on Rewriting Logic and its Applications (WRLA2000), Electronic Notes in Theoretical Computer Science. Elsevier Science, 2000.
[ps, pdf].

Jonathan Ford and Ian A. Mason.
Operational Techniques in PVS - A Preliminary Evaluation.
In Proceedings of the Australasian Theory Symposium, CATS '01, 2001.
[ps, pdf].

Jonathan Ford and Ian A. Mason.
Establishing a General Context Lemma in PVS.
In Proceedings of the 2nd Australasian Workshop on Computational Logic, AWCL'01 , 2001.
[ps, pdf].