Andre Scedrov's Selected Publications

The following list contains selected publications of Andre Scedrov, partially supported by the Office of Naval Research, by the Air Force Office of Scientific Research, by National Science Foundation, and earlier by a Centennial Research Fellowship from the American Mathematical Society, by a Senior Fellowship from the Japan Society for the Promotion of Science, and by the Visiting Scientist Program of the Dynasty Foundation. Any opinions, findings, and conclusions or recommendations expressed in these publications are those of the authors and do not necessarily reflect the views of the funding agencies. The files are also available from an ftp directory. Most of the papers available from this document appear in print and the corresponding copyright is held by the publisher. While the papers may be used for personal use, redistribution or reprinting for commercial purposes is not allowed.

Please also consult Andre Scedrov's dblp Computer Science Bibliography and Google Scholar entries.

Discrete vs. Dense Times in the Verification of Cyber-Physical Security Protocols (with M. Kanovich, T. Ban Kirigin, V. Nigam, and C. Talcott). In: R. Focardi and A. Myers, eds., 4th Conference on Principles of Security and Trust (POST 2015), London, UK, April, 2015, accepted.

Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds (with G. Barthe, E. Fagerholm, D. Fiore, B. Schmidt, and M. Tibouchi). In: J. Katz, ed., IACR International Conference on Practice and Theory of Public-Key Cryptography (PKC 2015), Gaithersburg, Maryland, USA, March 30 - April 1, 2015, accepted.

Automated Analysis of Cryptographic Assumptions in Generic Group Models (with G. Barthe, E. Fagerholm, D. Fiore, J.C. Mitchell and B. Schmidt). In: J. Garay and R. Gennaro, eds., 34th International Cryptology Conference (CRYPTO 2014), Proceedings, Part I, Santa Barbara, California, USA, August 2014. Springer LNCS Volume 8616, Springer-Verlag, 2014, pp. 95 - 112. ePrint Archive: Report 2014/458.

Bounded Memory Protocols (with M. Kanovich, T. Ban Kirigin, and V. Nigam). Computer Languages, Systems and Structures 40(3-4) (2014) 137 - 154 [.pdf]. Extended abstract under the title "Bounded Memory Protocols and Progressing Collaborative Systems" in: J. Crampton, S. Jajodia and K. Mayes, eds., The 18th European Symposium on Research in Computer Security (ESORICS 2013), Egham, UK, September 2013. Springer LNCS Volume 8134, Springer-Verlag, 2013, pp. 309 - 326.

Bounded Memory Dolev-Yao Adversaries in Collaborative Systems (with M. Kanovich, T. Ban Kirigin, and V. Nigam). Information and Computation 238 (2014) 233-261. Extended abstract in: P. Degano et al., eds., The 7th International Workshop on Formal Aspects of Security & Trust (FAST2010), Pisa, Italy, September 2010. Springer LNCS Volume 6561, Springer-Verlag, 2011, pp. 18-33. [.pdf].

A Reduction-based Approach Towards Scaling Up Formal Analysis of Internet Configurations (with A. Wang, A.J.T. Gurney, X. Han, J. Cao, B. Thau Loo, and C. Talcott). In: G. Bianchi, Y. Fang, and X. Shen, eds., 33rd Annual IEEE International Conference on Computer Communications (INFOCOM 2014), Toronto, Canada, April 27 - May 2, 2014, IEEE, 2014, pp. 637 - 645.

When Not All Bits Are Equal: Worth-Based Information Flow (with M.S. Alvim and F.B. Schneider). In: M. Abadi and S. Kremer, eds., 3rd Conference on Principles of Security and Trust (POST 2014), Grenoble, France, April 2014. Springer LNCS Volume 8414, Springer-Verlag, 2014, pp. 120 - 139. Technical Report.

Automated Synthesis of Reactive Controllers for Software-Defined Networks (with A. Wang, S. Moarref, B. Thau Loo, and U. Topcu). In: 3rd International Workshop on Rigorous Protocol Engineering (WRiPE 2013), 21st IEEE International Conference on Network Protocols (ICNP 2013), Goettingen, Germany, October 2013. IEEE Xplore Digital Library 2013. [.pdf].

FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing (with A. Wang, L. Jia, W. Zhou, Y. Ren, B. Thau Loo, J. Rexford, V. Nigam, and C. Talcott). IEEE/ACM Transactions on Networking 20(6) (2012) 1814-1827.

Reduction-based analysis of BGP systems with BGPVerif (with A. Wang, A.J.T. Gurney, X. Han, J. Cao, C.L. Talcott, and B. Thau Loo). Demo in: L. Eggert, J. Ott, V.N. Padmanabhan, G. Varghese, eds., ACM SIGCOMM 2012 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication. Helsinki, Finland, August 2012. ACM Press, 2012, pp. 89-90. [.pdf].

Brief Announcement: A Calculus of Policy-Based Routing Systems (with A. Wang, C.L. Talcott, A.J.T. Gurney, and B. Thau Loo). In: A. Panconesi, ed., 31-st Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC 2012). Madeira, Portugal, July 2012. ACM Press, 2012, pp. 343 - 344. [.pdf].

A Rewriting Framework for Activities Subject to Regulations (with M.I. Kanovich, T. Ban Kirigin, V. Nigam, C.L. Talcott, and R. Perovic). In: A. Tiwari, ed., 23-rd International Conference on Rewriting Techniques and Applications (RTA 2012). Nagoya, Japan, May 28 -June 2, 2012. Leibniz International Proceedings in Informatics Volume 15, Schloss Dagstuhl - Leibniz Center for Informatics, 2012, pp. 305 - 322. [.pdf].

Reduction-based Formal Analysis BGP Instances (with A. Wang, C.L. Talcott, A.J.T. Gurney, and B. Thau Loo). In: C. Flanagan and B. Koenig, eds., 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012). Tallinn, Estonia, March 2012. Springer LNCS Volume 7214, Springer-Verlag, 2012, pp. 283 - 298. Technical Report.

Declarative privacy policy: Finite models and attribute-based encryption (with P.E. Lam, J.C. Mitchell, S. Sundaram, and F. Wang). In: C.C. Yang, ed., 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, Florida, USA, January 2012. ACM Digital Library, 2012, pp. 323-332. [.pdf].

Towards an Automated Assistant for Clinical Investigations (with V. Nigam, T. Ban Kirigin, C. Talcott, M. Kanovich, and R. Perovic). In: C.C. Yang, ed., 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, Florida, USA, January 2012. ACM Digital Library, 2012, pp. 773-778. [.pdf].

Maintaining Distributed Logic Programs Incrementally (with V. Nigam, L. Jia, and B. Thau Loo). Computer Languages, Systems and Structures 38 (2012) 158-180. Extended abstract in: M. Hanus, ed., 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011). Odense, Denmark, July 2011. ACM Press, 2011, pp. 125-136. [.pdf].

Analyzing BGP Instances in Maude (with A. Wang, C.L. Talcott, L. Jia, and B. Thau Loo). In: R. Bruni and J. Dingel, eds., Formal Techniques for Distributed Systems. Joint 13th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems and 31st IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FMOODS & FORTE 2011), Reykjavik, Iceland, June 2011, Proceedings. Springer LNCS Volume 6722, Springer-Verlag, 2011, pp. 334 - 348. Technical report [.pdf].

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos (with M. Backes, I. Cervesato, A.D. Jaggard, and J.-K. Tsay). International Journal of Information Security 10(2) (2011) 107-133 [.pdf]. Extended astract in: D. Gollmann, J. Meier, and A. Sabelfeld, eds., "Computer Security - ESORICS 2006, 11-th European Symposium On Research In Computer Security", Hamburg, Germany, September 2006. Springer LNCS Volume 4189, Springer-Verlag, 2006, pp. 362 - 383.

Collaborative Planning with Confidentiality (with M. Kanovich and P. Rowe). Journal of Automated Reasoning 46 (3-4) (2011) 389-421. [.pdf]. Extended abstract under the title "Collaborative Planning with Privacy" in: A. Sabelfeld, ed., "20-th IEEE Computer Security Foundations Symposium (CSF)", Venice, Italy, July 2007. IEEE Computer Society Press, 2007, pp. 265-278.

An Operational Semantics for Network Datalog (with V. Nigam, L. Jia, A. Wang, and B. Thau Loo). In: B. Mueller (Farwer), ed., Third International Workshop on Logics, Agents, and Mobility (LAM'10). [.pdf].

Policy Compliance in Collaborative Systems (with M. Kanovich and P. Rowe). [.pdf]. In: J. Mitchell, ed., "22-nd IEEE Computer Security Foundations Symposium (CSF)", Port Jefferson, New York, USA, July 2009. IEEE Computer Society Press, 2009, pp. 218-233.

Refining Computationally Sound Mechanized Proofs for Kerberos (with B. Blanchet, A.D. Jaggard, J. Rao, and J.-K. Tsay). In: R. Kuesters, ed., "Workshop on Formal and Computational Cryptography (FCC 2009)", Port Jefferson, New York, USA, July 2009.

Relating State-Based and Process-Based Concurrency through Linear Logic (with I. Cervesato). Information and Computation 207(10) (2009) 1044-1077. [.pdf]. Extended abstract in: R. de Queiroz and G. Mints, eds., "13-th Workshop on Logic, Language, Information and Computation", Stanford, California, July 2006. ENTCS Volume 165, Elsevier, 2006, pp. 145-176.

Soundness and completeness of formal encryption: The cases of key-cycles and partial information leakage (with P. Adão, G. Bana, and J. Herzog). Journal of Computer Security 17(5) (2009) 737-797. [.pdf]. Extended abstract under the title "Soundness of formal encryption in the presence of key-cycles" in: S. De Capitani di Vimercati, P. Syverson, and D. Gollmann, eds., " 10-th European Symposium on Research in Computer Security (ESORICS 2005)", Milan, Italy, September 2005. Springer LNCS Volume 3679, Springer-Verlag, 2005, pp. 374-396.

Analysis of EAP-GPSK Authentication Protocol (with J.C. Mitchell, P. Rowe, and A. Roy). In: S. Bellovin and R. Gennaro, eds., "6-th International Conference on Applied Cryptography and Network Security (ACNS'08)", New York, June 2008. Springer LNCS Volume 5037, Springer-Verlag, 2008, pp. 309 - 327. [.pdf].

Computationally Sound Mechanized Proofs for Basic and Public-Key Kerberos (with B. Blanchet, A.D. Jaggard, and J.-K. Tsay). In: V. Gligor and M. Abe, eds., "ACM Symposium on Information, Computer and Communications Security (ASIACCS '08)", Tokyo, Japan, March 2008. ACM Press, 2008, pp. 87-99. ACM Portal link.

Key-dependent Message Security under Active Attacks - BRSIM/UC-Soundness of Dolev-Yao-style Encryption with Key Cycles (with M. Backes and B. Pfitzmann). Journal of Computer Security 16(5) (2008) 497-530. Extended abstract under the title "Key-dependent Message Security under Active Attacks - BRSIM/UC-Soundness of Symbolic Encryption with Key Cycles" in: A. Sabelfeld, ed., "20-th IEEE Computer Security Foundations Symposium (CSF)", Venice, Italy, July 2007. IEEE Computer Society Press, 2007, pp. 112-124. Preliminary version in: Cryptology ePrint Archive: Report 2005/421.

Breaking and fixing public-key Kerberos (with I. Cervesato, A.D. Jaggard, J.-K. Tsay, and C. Walstad). Information and Computation 206(2-4) (2008) 402-424. Extended abstract in: M. Okada, I. Satoh, eds., Advances in Computer Science - ASIAN 2006, Tokyo, Japan, December 2006. Springer LNCS Volume 4435, Springer-Verlag, 2008. Preliminary version [.pdf].

The work of Dean Rosenzweig: A Tribute to a Scientist and an Innovator. In: "Foundations of Software Engineering. 6-th Joint Meeting of the European Software Engineering Conference and the 14-th ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2007)", Dubrovnik, Croatia, September 2007, ACM Press, 2007, pp. 371-374. ACM Portal link.

Software Quality and Infrastructure Protection for Diffuse Computing (with J. Feigenbaum, J.Y. Halpern, P.D. Lincoln, J.C. Mitchell, J.M. Smith, and P. Syverson. In: C. Wang, S. King et al., eds., "Information Security Research", Wiley, 2007. ISBN: 978-0-471-78756-3.

Formal Analysis of Kerberos 5 (with F. Butler, I. Cervesato, A.D. Jaggard, and C. Walstad). [.pdf]. Theoretical Computer Science 367(1-2) (2006) 57-87.

Games and the Impossibility of Realizable Ideal Functionality (with A. Datta, A. Derek, J.C. Mitchell, and A. Ramanathan). In: S. Halevi and T. Rabin, eds., " 3-rd Theory of Cryptography Conference (TCC 2006)", New York, NY, March 2006. Springer LNCS Volume 3876, Springer-Verlag, 2006, pp. 360-379. Revised version in Cryptology ePrint Archive: Report 2005/211.

A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols (with J.C. Mitchell, A. Ramanathan, and V. Teague). Theoretical Computer Science 353 (2006) 118-164. [.pdf] [.ps] [.ps.gz]

Computational and information-theoretic soundness and completeness of formal encryption (with P. Adão and G. Bana). In: J. Guttman, ed., " 18-th IEEE Computer Security Foundations Workshop (CSFW)", Aix-en-Provence, France, June 2005. IEEE Computer Society Press, 2005, pp. 170-184. [.pdf] [.ps] [.ps.gz]

Specifying Kerberos 5 cross-realm authentication (with I. Cervesato, A. Jaggard, and C. Walstad). In: C. Meadows, ed., "Proceedings of the 2005 workshop on Issues in the theory of security (WITS'05)", Long Beach, California, January 2005. ACM Digital Library, ACM Press, New York, 2005, pp. 12-26. [.pdf]

Formal analysis of multi-party contract signing (with R. Chadha and S. Kremer). Journal of Automated Reasoning 36(1-2) (2006) pp. 39-83. [.pdf] [.ps] [.ps.gz] Preliminary report in: R. Focardi, ed., " 17-th IEEE Computer Security Foundations Workshop (CSFW)", Pacific Grove, California, June 2004. IEEE Computer Society Press, 2004, pp. 266-279. [.pdf] [.ps] [.ps.gz]

A formal analysis of some properties of Kerberos 5 using MSR (with F. Butler, I. Cervesato, and A. Jaggard). University of Pennsylvania Department of Computer and Information Science Technical Report MS-CIS-04-04, April 2004, 59 pages. [.pdf] [.ps] [.ps.gz]

Verifying Confidentiality and Authentication in Kerberos 5 (with F. Butler, I. Cervesato, and A. Jaggard). In: K. Futatsugi, F. Mizoguchi, N. Yonezaki, eds., "Software Security - Theories and Systems Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003" Springer LNCS Volume 3233, Springer-Verlag, 2004, pp. 1-24.

Probabilistic bisimulation and equivalence for security analysis of network protocols (with A. Ramanathan, J. Mitchell, and V. Teague). In: I. Walukiewicz, ed., "Foundations of Software Science and Computation Structures, 7-th International Conference, FOSSACS 2004", Springer LNCS Volume 2987, Springer-Verlag, 2004, pp. 468-483. Full, revised version [.pdf] [.ps] [.ps.gz]

Composition of cryptographic protocols in a probabilistic polynomial-time process calculus (with P. Mateus and J.C. Mitchell). In: R. Amadio and D. Lugiez, eds., "CONCUR 2003 - Concurrency Theory, 14-th International Conference, Marseille, France, September 2003", Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 327-349. [.pdf] [.ps] [.ps.gz]

Contract signing, optimism, and advantage (with R. Chadha, J.C. Mitchell, and V. Shmatikov). Journal of Logic and Algebraic Programming, Special issue on Modelling and Verification of Cryptographic Protocols, R.M. Amadio, ed., 64(2), 2005, pp. 189-218. [.pdf] [.ps] [.ps.gz] Extended abstract in: R. Amadio and D. Lugiez, eds., "CONCUR 2003 - Concurrency Theory, 14-th International Conference, Marseille, France, September 2003", Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 366-382.

A revised comparison between strand spaces and multiset rewriting for security protocol analysis (with I. Cervesato, N.A. Durgin, P.D. Lincoln, and J.C. Mitchell). Journal of Computer Security 13(2) (2005) 265-316. [.pdf] Extended abstract in: M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, eds., "Software Security - Theories and Systems. Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers", Springer LNCS Volume 2609, Springer-Verlag, 2003, pp. 356-383. Revised and expanded version of the preliminary report under the title "Relating strands and multiset rewriting for security protocol analysis" from: P. Syverson, ed., "13-th IEEE Computer Security Foundations Workshop, Cambridge, England, July, 2000", IEEE Computer Society Press, 2000, pp. 35-51.

A formal analysis of some properties of Kerberos 5 using MSR (with F. Butler, I. Cervesato, and A. Jaggard). In: S. Schneider, ed., "15-th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, June, 2002", IEEE Computer Society Press, 2002, pp. 175-190. Preliminary version [.pdf] [.ps] [.ps.gz].

Multiset rewriting and the complexity of bounded security protocols (with N. Durgin, P. Lincoln, and J. Mitchell). Journal of Computer Security 12(2), 2004, pp. 247-311. [.pdf] [.ps] [.ps.gz]. Preliminary report under the title Undecidability of bounded security protocols in: "Workshop on Formal Methods and Security Protocols (FMSP'99)", The 1999 Federated Logic Conference (FLoC'99), Trento, Italy, July, 1999.

A probabilistic polynomial-time calculus for analysis of cryptographic protocols (with J. Mitchell, A. Ramanathan, and V. Teague). Preliminary report, 2001, 25 pages. [.pdf] [.ps] [.ps.gz]. In: S. Brookes, M. Mislove, eds., "17-th Annual Conference on the Mathematical Foundations of Programming Semantics", Arhus, Denmark, 2001, Electronic Notes in Theoretical Computer Science, Volume 45 (2001).

Inductive methods and contract-signing protocols (with R. Chadha and M.I. Kanovich). In: P. Samarati, ed., "8-th ACM Conference on Computer and Communications Security, Philadelphia, Pennsylvania, November, 2001", ACM Press, 2001, pp. 176-185. Extended version [.pdf] [.ps] [.ps.gz].

Interpreting strands in linear logic (with I. Cervesato, N.A. Durgin, and M.I. Kanovich). In: "2000 Workshop on Formal Methods and Computer Security", 12th International Conference on Computer Aided Verification (CAV 2000) Satellite Workshop, Chicago, Illinois, July, 2000.

Probabilistic polynomial-time equivalence and security analysis (with P.D. Lincoln, J.C. Mitchell, and M. Mitchell). In: J.M. Wing, J. Woodcock, J. Davies (Eds.), FM'99 - Formal Methods World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999. Proceedings, Volume I, Springer Lecture Notes in Computer Science, vol. 1708, 1999, pp. 776-793. Revised version.

A meta-notation for protocol analysis (with I. Cervesato, N.A. Durgin, P.D. Lincoln, and J.C. Mitchell). In: P. Syverson, ed., "12-th IEEE Computer Security Foundations Workshop, Mordano, Italy, June, 1999", IEEE Computer Society Press, 1999, pp. 55-69.

A probabilistic poly-time framework for protocol analysis (with P.D. Lincoln, J.C. Mitchell, and M. Mitchell). In: M. Reiter, ed., "5-th ACM Conference on Computer and Communications Security, San Francisco, California, November, 1998", ACM Press, 1998, pp. 112-121.

A linguistic characterization of bounded oracle computation and probabilistic polynomial time (with J.C. Mitchell and M. Mitchell). In: R. Motwani, ed., "39-th Annual IEEE Symposium on Foundations of Computer Science (FOCS)", Palo Alto, California, November, 1998", IEEE Computer Society Press, 1998, pp. 725-733.

Specifying Real-Time Finite-State Systems in Linear Logic (with M.I. Kanovich and M. Okada). In: "2-nd International Workshop on Constraint Programming for Time-Critical Applications and Multi-Agent Systems (COTIC)", Nice, France, September, 1998, Electronic Notes in Theoretical Computer Science, Volume 16 Issue 1 (1998) 15 pp.

Phase Semantics for Light Linear Logic (with M.I. Kanovich and M. Okada). Theoretical Computer Science Volume 294 Issue 3 (2003) pp. 525-549. Extended abstract in: "13-th Annual Conference on the Mathematical Foundations of Programming Semantics", Pittsburgh, Pennsylvania, March, 1997, Electronic Notes in Theoretical Computer Science, Volume 6 (1997) 12 pp.

Optimization Complexity of Linear Logic Proof Games (with P.D. Lincoln and J.C. Mitchell). Theoretical Computer Science 227 (1999) pp. 299-331. Extended abstract under the title "The Complexity of Local Proof Search in Linear Logic" in: "Proceedings Linear Logic '96, Tokyo Meeting", Electronic Notes in Theoretical Computer Science, Volume 3 (1996) 10 pp.

Linear Logic Proof Games and Optimization, (with P.D. Lincoln and J.C. Mitchell). Bulletin of Symbolic Logic 2 (1996) pp. 322-338.

The Undecidability of Second Order Multiplicative Linear Logic, (with Y. Lafont). Information and Computation 125 (1996) pp. 46-51. LMD Marseille Preprint 95-17, March, 1995.

Decision Problems for Second Order Linear Logic, (with P. Lincoln and N. Shankar). In: "Logic and Scientific Methods", ed. by M.L. Dalla Chiara et al., Kluwer Academic Publishers, 1997, pp. 127-143. Extended abstract in: "10-th Annual IEEE Symposium on Logic in Computer Science", San Diego, California, June, 1995, IEEE Computer Society Press, 1995, pp. 476-485.

Stochastic Interaction and Linear Logic, (with P. Lincoln and J.C. Mitchell). In: "Advances in Linear Logic", ed. by J.-Y. Girard, Y. Lafont, and L. Regnier, London Mathematical Society Lecture Notes Series, Volume 222, Cambridge University Press, 1995, pp. 147-166.

Linear Logic and Computation: A Survey. In: "Proof and Computation", ed. by H. Schwichtenberg, NATO Advanced Science Institutes, Series F, Volume 139, Springer-Verlag, Berlin, 1995, pp. 379-395.

First Order Linear Logic Without Modalities is NEXPTIME-Hard, (with P. Lincoln). Theoretical Computer Science 135 (1994) pp. 139-154.

An Extension of System F with Subtyping, (with L. Cardelli, J.C. Mitchell, and S. Martini). Information and Computation 109 (1994) pp. 4-56.

Notes on Sconing and Relators, (with J.C. Mitchell). In: "Computer Science Logic '92, Selected Papers", ed. by E. Boerger et al., Springer LNCS 702, 1993, pp. 352-378.

A Brief Guide to Linear Logic. In: "Current Trends in Theoretical Computer Science", ed. by G. Rozenberg and A. Salomaa, World Scientific Publishing Co., 1993, pp. 377-394.

Linearizing Intuitionistic Implication, (with P. Lincoln and N. Shankar). Annals of Pure and Applied Logic 60 (1993) pp. 151-177.

Grothendieck Topoi Representing Models of Set Theory, (with A. Blass). Annals of Pure and Applied Logic 57 (1992) pp. 1-26.

Decision Problems for Propositional Linear Logic, (with P. Lincoln, J.C. Mitchell, and N. Shankar). Annals of Pure and Applied Logic 56 (1992) pp. 239-311, Special Volume dedicated to the memory of John Myhill.

Bounded Linear Logic: A Modular Approach to Polynomial Time Computability , (with J.-Y. Girard and P.J. Scott). Theoretical Computer Science 97 (1992) pp. 1-66.

Normal Forms and Cut-Free Proofs as Natural Transformations, (with J.-Y. Girard and P.J. Scott). In: "Logic From Computer Science, Mathematical Sciences Research Institute Workshop, Berkeley, November, 1989", ed. by Y.N. Moschovakis, MSRI Publications, Vol. 21, Springer-Verlag, 1992, pp. 217-241.

Inheritance as Implicit Coercion, (with V. Breazu-Tannen, T. Coquand, and C.A. Gunter). Information and Computation 93 (1991) pp. 172-221.

Uniform Proofs as a Foundation for Logic Programming, (with D. Miller, G. Nadathur, and F. Pfenning). Annals of Pure and Applied Logic 51 (1991) pp. 125-157.

Functorial Polymorphism, (with E.S. Bainbridge, P.J. Freyd, P.J. Scott). Theoretical Computer Science 70 (1990) pp. 35-64.

"Categories, Allegories", (with P.J. Freyd). North-Holland Mathematical Library, North-Holland, Amsterdam, 1990, xviii + 296 pp.