@TechReport{MM01:secsafe, author = "R. Marlet and D. Le M\'{e}tayer", title = "Security Properties and Java Card Specificities to be Studied in the SecSafe Project", institution = "Trusted Logic S.A.", year = "2001", number = "SECSAFE-TL-006", month = aug} @TechReport{gerardo04:tr, author = {G. Schneider}, title = "A constraint-based algorithm for analysing memory usage on Java cards", institution = {INRIA}, year = {2004}, number = {RR-5440} } @misc{BCM05:fcs, author={R. Medel and E. Bonelli and A. Compagnoni}, title={{SIFTAL: A Typed Assembly Language for Secure Information Flow Analysis}}, year={2005}, note={Manuscript. To be presented at FCS'05}} @techreport{JP03:loop, title="{Java Program Verification at Nijmegen: Developments and Perspective}", author={B.P.F. Jacobs and E. Poll}, year=2003, institution="NIII, Katholieke Universiteit Nijmegen", number={NIII-R0318}} @techreport{jml:prelim, Author = "G.T. Leavens and A.L. Baker and C. Ruby", Title = "{Preliminary Design of JML: a Behavioral Interface Specification Language for Java}", Institution = "Iowa State University, Department of Computer Science", Year = 1998, number = "98-06"} @techreport{LBW03:tr, title={Edit Automata: Enforcement Mechanisms for Run-time Security Policies}, author={J. Ligatti and L. Bauer and D. Walker}, year={2003}, institution={Department of Computer Science, Princeton University}, number={TR-681-03}} @TechReport{BP75:tr, author = "D. Bell and L. LaPadula", title = "Secure Computer Systems: Unified Exposition and Multics Interpretation", year = "1975", month = jul, number = "MTR-2997", institution = "{MITRE} Corporation" } @TechReport{car86:typeintype, author = "L. Cardelli", title = "{A polymorphic lambda-calculus with Type:Type}", institution={SRC}, number={10}, year={1986}, month=may} @TechReport{adriana:tr, author = {Compagnoni, A. and Goguen, H.}, title = {Typed Operational Semantics for Higher Order Subtyping}, institution = {University of Edinburgh}, year = 1997, number = "ECS-LFCS-97-361", month = jul} @TechReport{cra99:tr, author={K. Crary}, title={Simple, Efficient Object Encoding using Intersection Types}, institution={Carnegie-Mellon University}, number={CMU-CS-99-100}, year={1999}} @techreport{eduardo:tutorial, title={A tutorial on recursive types in Coq}, author={E. Gim{\'e}nez}, institution={INRIA}, number={RT-0221}, year={1998}} @techreport{FW97:tr, author={M. Fairtlough and M. Walton}, title="Quantified Lax Logic", number={CS-97-11}, institution={Department of Computer Science, University of Sheffield}, year={1997}} @techreport{gou:tr, author={J. Goubault-Larrecq}, title={On Computational Interpretations of the Modal Logic S4}, institution={University of Karlsruhe}, year={1996}, month=jul} @techreport{HMS03:tr, title={Computability Classes for Enforcement Mechanisms}, institution={Department of Computer Science, Cornell University}, number={2003-1908}, year={2003}, author={K. Hamlen and G. Morrisett and F.B. Schneider}} @techreport{JLMT98:tr, author={T. Jensen and D. Le M\'etayer and T. Thorn}, title={Verification of Control Flow Based Security Properties}, institution={IRISA}, number={1210}, year={1998}, month=oct} @techreport{low99:tr, author={G. Lowe}, title={Defining Information Flow}, institution={Department of Mathematics and Computer Science, University of Leicester}, number={1999/3}, year=1999} @TECHREPORT{LR96:tr, author={B. Luttik and P. Rodenburg}, title={Transformations of reduction systems}, year={1996}, institution={University of Amsterdam}, type={Technical Reports of the Programming Research Group}, number={P9615}} @techreport{nau03:pvs, author={D. Naumann}, title={Machine-checked correctness of a secure information flow analyzer (preliminary report)}, year={2003}, month=mar, number={CS-2004-10}, institution={Stevens Institute of Technology}} @techreport{erik:bij, author={E. Poll}, title={A Typechecker for Bijective Pure Type Systems}, year={1993}, month={June}, institution={Technical University of Eindhoven}, number={CSN93/22}} @TECHREPORT{PBJ00:api, author={E. Poll and J. van den Berg and B. Jacobs}, title={{Specification of the JavaCard API in JML}}, institution={Computing Science Institute, University of Nijmegen}, number={Technical Report CSI-R0005}, year={2000}, month=mar, note={To appear in the Proceedings of CARDIS'00}} @TECHREPORT{femkepaula, AUTHOR = "Raamsdonk, F. van and Severi, P.", TITLE = "On Normalisation", INSTITUTION = "CWI", NUMBER = "CS-R9545", MONTH = jun, YEAR = 1995 } @TechReport{rei89:tr, number = "MIT/LCS/TR-458", title = "Typechecking is undecidable '{TYPE}' is a type", month = dec, year = "1989", author = "M. B. Reinhold", institution = "Massachusetts Institute of Technology", } @techreport{rus93:fm, AUTHOR = {J. Rushby}, TITLE = {Formal Methods and the Certification of Critical Systems}, INSTITUTION = {Computer Science Laboratory, SRI International}, YEAR = 1993, NUMBER = {SRI-CSL-93-7}, ADDRESS = {Menlo Park, CA}, NOTE = {Also issued under the title {\em Formal Methods and Digital Systems Validation for Airborne Systems\/} as NASA Contractor Report 4551, December 1993. A book based on this material will be published by Cambridge University Press in 1996/7}, MONTH = dec } @techreport{rus92:sri, AUTHOR = {J. Rushby}, TITLE = {Noninterference, Transitivity, and Channel-Control Security Policies}, YEAR = {1992}, MONTH = {dec}, URL = {http://www.csl.sri.com/papers/csl-92-2/}, number ={{SRI-CSL-92-02}}, INSTITUTION = {Computer Science Laboratory, SRI International}, } @TechReport{shaoetal01:certbin, title={A Type System for Certified Binaries}, author={Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou}, number={YALEU/DCS/TR-1211}, institution={Department of Computer Science, Yale University}, month=jul, year={2001}} @TechReport{SU98:ch, AUTHOR = {S{\o}rensen, M. H. and Urzyczyn, P.}, YEAR = {1998}, TITLE = {Lectures on the Curry-Howard Isomorphism}, number={98/14}, institution={DIKU}, } @TechReport{sch99:esp, author = {F. B. Schneider}, title = {Enforceable security policies}, institution = {Cornell University}, year = {1999}, number = {TR99-1759}, month = {October} } @TechReport{sch:brar, author={Schmidt, D.A.}, title={Binary relations for abstraction and refinement}, institution={Department of Computing and Information Sciences, Kansas State University}, number={2000-3}, year={2000}} @TechReport{str03:ni, author = {M. Strecker}, title = {Formal Analysis of an Information Flow Type System for {M}icro{J}ava (Extended Version)}, institution = {Technische Universit{\"a}t M{\"u}nchen}, year = 2003, month = jul } @TechReport{GLV:tr, author = "Verma, K. N. and Goubault-Larrecq, J.", title = "Reflecting {BDDs} in {Coq}", number={RR3859}, institution = "INRIA projet Coq", year =2000, month =jan } %%%%%%%%%%%%%%%%% stopped here %%%%%%%%%%%%%%%%%%%%%% @TECHREPORT{FvdP96:tr, author={W. Fokkink and J. van de Pol}, title={Correct transformations of rewrite systems for implementation purposes}, year={1996}, institution={Univeristy of Utrecht}, type={Logic Group Preprint Series}, number={164}} @TECHREPORT{pit95:tr, AUTHOR={A.~Pitts}, TITLE={Categorical Logic}, INSTITUTION={University of Cambridge Computer Laboratory}, YEAR=1995, TYPE={Technical Report}, NUMBER=367, MONTH=may} @techreport{bie96:cll, author="G.M.~Bierman", title="A Classical Linear $\lambda$-calculus", institution="University of Cambridge Computer Laboratory", number=401, month=jul, year=1996 } @techreport{chen96:tr, author={G. Chen}, title={{Dependent Type System with Subtyping. Type level transitivity elimination}}, institution={Ecole Normale Superieure}, number={LIENS-96-27}, year={1996}} @techreport{ML72:tr, author={P. Martin-L{\"o}f}, title={An Intuitionistic Theory of Types}, institution={University of Stockholm}, number={TR 72-?}, year={1972}} @Techreport{mun99:sri, Author = "C. Mu{\~{n}}oz", Title = "{PBS}: Support for the {B}-Method in {PVS}", Institution = {SRI International}, Month = {February}, Number = {SRI-CSL-99-01}, Year = {1999}} @techreport{pot87:tr, author={G. Pottinger}, title={Strong normalisation for terms of the theory of constructions}, institution={Odissey Research Associates}, number={TR 11-7}, year={1987}} @techreport{bas95:tr, author={T.J. Bastiansen}, title={Parametric subtypes in {ABEL}}, institution={{Department of Informatics, University of Oslo}}, number={207}, year={1995}} @techreport{DO95:tr, author={O-J. Dahl and O. Owe}, title={On the use of subtypes in {ABEL}}, institution={{Department of Informatics, University of Oslo}}, number={206}, year={1995}} @techreport{DCK93, author = "Di Cosmo, R. and Kesner, D.", title = "Simulating expansions without expansions", institution = "INRIA Rocquencourt", number = 1991, year = 1993, } @TechReport{isabelle:intro, author = "L.C. Paulson", title = "Introduction to {Isabelle}", institution = "University of Cambridge, Computer Laboratory", year = 1993, number = 280, } @TechReport{har:refl, author = "J. Harrison", title = "Metatheory and Reflection in Theorem Proving: A Survey and Critique", institution = "SRI Cambridge, UK", year = 1995, number = "CRC-053" } @TECHREPORT{har:real , AUTHOR = {J. Harrison} , TITLE = {Constructing the Real Numbers in {HOL}} , INSTITUTION = {University of Cambridge, Computer Laboratory} , YEAR = 1993 } @techreport{gun, author={E. Gunter}, title={Doing algebra in simple type theory}, institution={Department of Computer and Information Science, University of Pennsylvania}, year={1989}, number={MS-CIS-89-38}} @techreport{SP94, author={M. Steffen and B. Pierce}, title={Higher-order subtyping}, institution=lfcs, year={1994}, number={ECS-LFCS-94-280}} @techreport{milena95, author={M. Stefanova}, title={Schematic proof of strong normalisation for the systems of the $\lambda$-cube}, institution={Department of Computer Science, University of Nijmegen}, year={1996}, note={In preparation}} @TECHREPORT{Wells:UMSR-1995, AUTHOR = {J. B. Wells}, TITLE = {The Undecidability of {Mitchell's} Subtyping Relation}, INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.}, YEAR = 1995, MONTH = DEC, DOCUMENTURL = {http://www.church-project.org/reports/Wells:UMSR-1995.html}, POSTSCRIPT = {http://www.cs.bu.edu/ftp/pub/jbw/types/subtyping-undecidable.ps.gz}, POSTSCRIPTB = {http://www.cs.bu.edu/techreports/ps/1995-019-subtyping-undecidable.ps.gz}, REMARK = {Doesn't have tech report number in the actual paper.}, TYPE = {Tech.\ Rep.}, NUMBER = {95-019}, CHURCHREPORT = {yes}, ABSTRACT = {Mitchell defined and axiomatized a subtyping relationship (also known as \emph{containment}, \emph{coercibility}, or \emph{subsumption}) over the types of System F (with ``$\to$'' and ``$\forall$''). This subtyping relationship is quite simple and does not involve bounded quantification. Tiuryn and Urzyczyn quite recently proved this subtyping relationship to be undecidable. This paper supplies a new undecidability proof for this subtyping relationship. First, a new syntax-directed axiomatization of the subtyping relationship is defined. Then, this axiomatization is used to prove a reduction from the undecidable problem of \emph{semi-unification} to subtyping. The undecidability of subtyping implies the undecidability of \emph{type checking} for System F extended with Mitchell's subtyping, also known as ``F plus eta''.} }