% James J. Leifer's bibliography @String{JJLHOME = "http://pauillac.inria.fr/{$\sim$}leifer/"} @String{CLUCAM = "Computer Laboratory, University of Cambridge"} @String{FAC = "Formal Aspects of Computing"} @String{INRIAROCQ = "INRIA Rocquencourt"} @String{JFP = "Journal of Functional Programming"} @String{LNCS = "Lecture Notes in Computer Science"} @String{MSCS = "Mathematical Structures in Computer Science"} @String{SPRINGER = "Springer-Verlag"} @Article{Leifer:1996:DFP, author = "James J. Leifer and Bernard A. Sufrin", title = "Deduction for functional programmers", journal = JFP, year = "1996", volume = "6", number = "2", pages = "365--373", note = "Available from " # JJLHOME, } @TechReport{Leifer:2000:CEC, author = "Gian Luca Cattani and James J. Leifer and Robin Milner", title = "Contexts and embeddings for closed shallow action graphs", institution = CLUCAM, year = "2000", number = "496", month = jul, note = "Available from " # JJLHOME, } @InProceedings{Leifer:2000:DBC, author = "James J. Leifer and Robin Milner", title = "Deriving bisimulation congruences for reactive systems", booktitle = "CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22--25, 2000, Proceedings", editor = "C. Palamidessi", volume = "1877", series = LNCS, year = "2000", pages = "243--258", publisher = SPRINGER, note = "Available from " # JJLHOME, } @PhdThesis{Leifer:2001:OCR, author = "James J. Leifer", title = "Operational congruences for reactive systems", school = CLUCAM, year = "2001", note = "Available in revised form as Technical Report 521," # CLUCAM # ", 2001, from " # JJLHOME, } @TechReport{Leifer:2001:CAG, author = "James J. Leifer", title = "A category of action graphs and reflexive embeddings", institution = CLUCAM, year = "2002", note = "Working note.", } @Article{Leifer:2002:SLA, author = "James J. Leifer and Robin Milner", title = "Shallow linear action graphs and their embeddings", journal = FAC, year = "2002", volume = "13", number = "3--5", note = "Special issue in honour of Rod Burstall. Available from " # JJLHOME, pages = "327--340", } @TechReport{Leifer:2002:SLT1, author = "James J. Leifer", title = "Synthesising labelled transitions and operational congruences in reactive systems, part~1", year = "2002", month = mar, institution = INRIAROCQ, number = "RR-4394", note = "Available from " # JJLHOME, } @TechReport{Leifer:2002:SLT2, author = "James J. Leifer", title = "Synthesising labelled transitions and operational congruences in reactive systems, part~2", year = "2002", month = mar, institution = INRIAROCQ, number = "RR-4395", note = "Available from " # JJLHOME, } @TechReport{Leifer:2003:GAS-inria, author = "James J. Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough", title = "Global abstraction-safe marshalling with hash types", institution = INRIAROCQ, number = "RR-4851", year = "2003", note = "Available from " # JJLHOME, } @InProceedings{Leifer:2003:GAS, author = "James J. Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough", title = "Global abstraction-safe marshalling with hash types", booktitle = "Proc.\@ 8th {ICFP}", year = "2003", note = "Available from " # JJLHOME, } @TechReport{Leifer:2004:TLG, author = "James J. Leifer and Robin Milner", title = "Transitions, link graphs and Petri nets", institution = CLUCAM, year = "2004", number = "598", note = "Available from " # JJLHOME, } @TechReport{Leifer:2004:AHL, author = "Peter Sewell and James J. Leifer and Keith Wansbrough and Mair Allen-Williams and Francesco Zappa Nardelli and Pierre Habouzit and Viktor Vafeiadis.", title = "Acute: High-level programming language design for distributed computation --- design rationale and language definition", year = "2004", month = oct, institution = INRIAROCQ, number = "RR-5329", note = "Available from " # JJLHOME, } @InProceedings{Leifer:2005:AHL-icfp, author = "Peter Sewell and James J. Leifer and Keith Wansbrough and Mair Allen-Williams and Francesco Zappa Nardelli and Pierre Habouzit and Viktor Vafeiadis.", title = "Acute: High-level programming language design for distributed computation", year = "2005", booktitle = "Proc.\@ 10th {ICFP}", note = "Available from " # JJLHOME, } @InProceedings{Leifer:2006:APS, author = "Pierre-Malo Deni{\'e}lou and James J. Leifer", title = "Abstraction preservation and subtyping in distributed languages", booktitle = "Proc.\@ 11th {ICFP}", year = "2006", note = "Available from " # JJLHOME, } @Article{Leifer:2006:TSL, author = "James J. Leifer and Robin Milner", title = "Transition systems, link graphs and Petri nets", journal = MSCS, year = "2006", volume = "16", number = "6", pages = "989--1047", note = "Available from " # JJLHOME, } @Article{Leifer:2007:AHL, author = "Peter Sewell and James J. Leifer and Keith Wansbrough and Francesco {Zappa Nardelli} and Mair Allen-Williams and Pierre Habouzit and Viktor Vafeiadis", title = "Acute: High-level programming language design for distributed computation", journal = JFP, year = "2007", volume = "17", number = "4-5", pages = "547--612", publisher = "Cambridge University Press", note = "Available from " # JJLHOME, } @InProceedings{Leifer:2007:SIT, author = "R. Corin and P. M. Denielou and C. Fournet and K. Bhargavan and J. Leifer", title = "Secure Implementations for Typed Session Abstractions", booktitle = "20th IEEE Computer Security Foundations Symposium (CSF'07)", pages = "170--186", year = "2007", address = "Venice, Italy", month = jul, organization = "IEEE", URL = "http://www.msr-inria.inria.fr/projects/sec/sessions/", abstract = "Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These sessions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant. In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low-level coding below session abstractions, thus giving up most of their benefits. We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well-typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low-level attempt by coalitions of remote peers to deviate from their roles. Our main result is that, when reasoning about programs that use our session implementation, one can safely assume that all session peers comply with their roles---without trusting their remote implementations.", note = "Available from " # JJLHOME, } @Article{Leifer:2008:SCS, author = "R. Corin and P. M. Denielou and C. Fournet and K. Bhargavan and J. Leifer", title = "A Secure Compiler for Session Abstractions", journal = "Journal of Computer Security", year = "2008", note = "To appear", note = "Available from " # JJLHOME, } % end