Call for Papers JOURNAL OF AUTOMATED REASONING Special issue on PROOF-CARRYING CODE Proof-carrying code is a technology that allows a host, or code consumer, to safely run code delivered by an untrusted code producer. The code producer delivers both a program and a formal proof that verifies that the code meets the desired safety policies. Safety policies generally express properties that prohibit the code from harmful behavior such as accessing private data, overwriting important data, accessing unauthorized resources, or consuming too many resources. Ideally, a proof is constructed automatically, and proof search may be directed using information that is passed on from the code producer's compiler. Proofs provided semi-automatically or interactively using a proof assistant are possible as well. Upon receiving the code and proof, the code consumer uses a mechanical proof checker to check the proof before executing the code. This special issue will be devoted to the topic of proof-carrying code and related approaches which use formal reasoning to enhance safety and reliability of software. Manuscripts emphasizing original results and study of tools and methods for proof generation, proof checking, and their integration with code generation/compilation are of particular interest. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. Information on JAR submissions can be found at URL http://www-unix.mcs.anl.gov/JAR/. Please format your submissions using JAR macros (available at http://www.wkap.nl/kaphtml.htm/STYLEFILES). Submissions should be sent to the guest editor in postscript format, preferably gzipped and uuencoded. In addition, please send as plain text, the title, authors, abstract, and contact information for the paper. The submission deadline is February 22, 2002. Guest Editor: Amy Felty, University of Ottawa, afelty@site.uottawa.ca This information is available on the web at: http://www.site.uottawa.ca/~afelty/jar-pcc/