With Ida
Alan Jeffrey
Member of Technical Staff
1960 Lucent Lane
Naperville, IL 60563, USA
Wordcloud

Bibliography

[ BibTeX | DBLP | Google Scholar | Microsoft Academic ]

Refereed Papers

  • Functional Reactive Types. A. S. A. Jeffrey. In Proc. EACSL Computer Science Logic / IEEE Logic in Computer Science. 2014. To appear. (PDF)

  • An Extensible Approach to Session Polymorphism. M. Goto, R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J Riely. In Math. Struct. in Comp. Science. 2014. To appear. (PDF)

  • Functional Reactive Programming with Liveness Guarantees. A. S. A. Jeffrey. In Proc. ACM Int. Conf. Functional Programming. 2013. (PDF)

  • Validation and Interactivity of Web API Documentation. P. J. Danielsen and A. S. A. Jeffrey. In Proc. IEEE Int. Conf. Web Services. 2013. (PDF)

  • Causality For Free!: Parametricity Implies Causality for Functional Reactive Programs. A. S. A. Jeffrey. In Proc. ACM Workshop Programming Languages meets Program Verification. 2013. (PDF)

  • Dependently Typed Web Client Applications: FRP in Agda in HTML5. A. S. A. Jeffrey. In Proc. Practical Aspects of Declarative Languages. 2013. (PDF)

  • As XDuce is to XML so ? is to RDF: Programming Languages for the Semantic Web. A. S. A. Jeffrey and P. F. Patel-Schneider. In Proc. Off The Beaten Track: Workshop on Underrepresented Problems for Programming Language Researchers. 2012. (PDF)

  • LTL Types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs. A. S. A. Jeffrey. In Proc. ACM Workshop Programming Languages meets Program Verification. 2012. (PDF)

  • The Lax Braided Structure of Streaming I/O. A. S. A. Jeffrey and J. Rathke. In Proc. Conf. Computer Science Logic. 2011. (PDF)

  • Integrity Constraints for Linked Data. A. S. A. Jeffrey and P. F. Patel-Schneider. In Proc. Int. Workshop Description Logics. 2011. (PDF)

  • Confidential Safety via Correspondence Assertions. R. Jagadeesan, A. Jeffrey, C. Pitcher and J. Riely. In Proc. Workshop Foundations of Security and Privacy. 2010. (PDF)

  • Towards a Theory of Accountability and Audit. R. Jagadeesan, A. Jeffrey, C. Pitcher and J. Riely. In Proc. European Symp. Research in Computer Security. Springer-Verlag. 2009. pp. 152-167. (PDF)

  • Model Checking Firewall Policy Configurations. A. S. A. Jeffrey and T. Samak. In Proc IEEE Int. Symp. Policies for Distributed Systems and Networks. 2009. pp. 60 -67. (PDF)

  • Stream Firewalling of XML Constraints. M. Benedikt, A. S. A. Jeffrey and R. Ley-Wild. In Proc. ACM SIGMOD Int. Conf. Management of Data. 2008. pp. 487-498. (PDF)

  • Lambda-RBAC: Programming with Role-Based Access Control. R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J. Riely. In Logical Methods In Computer Science. 4 (1). 2008. (PDF)

  • Efficient and Expressive Tree Filters. M. Benedikt and A. S. A. Jeffrey. In Proc. Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag. 2007. pp. 461-472. (PDF)

  • Full Abstraction for Polymorphic Pi-Calculus. A. S. A. Jeffrey and J. Rathke. In Theoretical Computer Science. 390 (2-3). 2008. pp. 171-196. (PDF)

  • Dynamic Model Checking of C Cryptographic Protocol Implementations. A. S. A. Jeffrey and R. Ley-Wild. In Proc. Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis. 2006. (PDF)

  • Pattern-Matching Spi-Calculus. C. Haack and A. S. A. Jeffrey. In Information and Computation. 204 (8). 2006. pp. 1195-1263. (PDF)

  • Typed Parametric Polymorphism for Aspects. R. Jagadeesan, A. S. A. Jeffrey and J. Riely. In Science of Computer Programming. 63 (3). 2006. pp. 267--296. (PDF)

  • Lambda-RBAC: Programming with Role-Based Access Control. R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J. Riely. In Proc. Int. Colloq. Automata, Languages and Programming. Springer-Verlag. 2006. pp. 456-467. Full version appeared in Logical Methods in Computer Science. (PDF)

  • Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus. A. D. Gordon and A. S. A. Jeffrey. In Proc. Concur. Springer-Verlag. 2005. pp. 186-201. (PDF)

  • Timed Spi-calculus with Types for Secrecy and Authenticity. C. Haack and A. S. A. Jeffrey. In Proc. Concur. Springer-Verlag. 2005. pp. 202-216. (PDF)

  • Contextual Equivalence for Higher-Order Pi-Calculus Revisited. A. S. A. Jeffrey and J. Rathke. In Logical Methods in Computer Science. 1 (1:4). 2005. pp. 1-22. (PDF)

  • Java Jr.: Fully Abstract Trace Semantics for a Core Java Language. A. S. A. Jeffrey and J. Rathke. In Proc. European Symposium on Programming. Springer-Verlag. 2005. pp. 423-438. (PDF)

  • Full Abstraction for Polymorphic Pi-Calculus. A. S. A. Jeffrey and J. Rathke. In Proc. Foundations of Software Science and Computation Structures. Springer-Verlag. 2005. pp. 266-281. Full version appeared in Theoretical Computer Science. (PDF)

  • Pattern-Matching Spi-Calculus. C. Haack and A. S. A. Jeffrey. In Proc. IFIP WG 1.7 Workshop on Formal Aspects in Security and Trust. 2004. Full version appeared in Information and Computation 204(8). (PDF)

  • A Fully Abstract May Testing Semantics for Concurrent Objects. A. S. A. Jeffrey and J. Rathke. In Theoretical Computer Science. vol. 338. 2005. pp. 17-63. (PDF)

  • muABC: A Minimal Aspect Calculus. G. Bruns, R. Jagadeesan, A. S. A. Jeffrey and J. Riely. In Proc. Concur. Springer-Verlag. 2004. pp. 209--224. (PDF)

  • Types and Effects for Asymmetric Cryptographic Protocols. A. D. Gordon and A. S. A. Jeffrey. In J. Computer Security. 12 (3/4). 2004. pp. 435-484. (PDF)

  • A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names. A. S. A. Jeffrey and J. Rathke. In Theoretical Computer Science. vol. 323. 2004. pp. 1-48. (PDF)

  • Authenticity by Typing for Security Protocols. A. D. Gordon and A. S. A. Jeffrey. In J. Computer Security. 11 (4). 2003. pp. 451-521. (PDF)

  • Typing Correspondence Assertions for Communication Protocols. A. D. Gordon and A. S. A. Jeffrey. In Theoretical Computer Science. vol. 300. 2003. pp. 379-409. (PDF)

  • SafetyNet: A Language-Based Approach to Programmable Networks. I. Wakeman, A. S. A. Jeffrey, T. Owen and D. Pepper. In Computer Networks and ISDN Systems. 36 (1). 2001.

  • A Calculus of Untyped Aspect-Oriented Programs. R. Jagadeesan, A. S. A. Jeffrey and J. Riely. In Proc. European Conf. Object-Oriented Programming. Springer-Verlag. 2003. pp. 415--427. (PDF)

  • Contextual Equivalence for Higher-Order Pi-Calculus Revisited. A. S. A. Jeffrey and J. Rathke. In Proc. Mathematical Foundations of Programming Semantics. Elsevier. 2003. Full version appeared in Logical Methods in Computer Science 1 (1:4). (PDF)

  • Types and Effects for Asymmetric Cryptographic Protocols. A. D. Gordon and A. S. A. Jeffrey. In Proc. IEEE Computer Security Foundations Workshop. IEEE Press. 2002. pp. 77-91. Full version appeared in J. Computer Security 12(3/4). (PDF)

  • Typing One-to-One and One-to-Many Correspondences in Security Protocols. A. D. Gordon and A. S. A. Jeffrey. In Proc. Int. Software Security Symp.. Springer-Verlag. 2002. pp. 263-282. (PDF)

  • A Fully Abstract May Testing Semantics for Concurrent Objects. A. S. A. Jeffrey and J. Rathke. In Proc. IEEE Logic In Computer Science. IEEE Press. 2002. pp. 101-112. Full version appeared in Theoretical Computer Science 338. (PDF)

  • A Symbolic Labelled Transition System for Coinductive Subtyping of F-mu-sub Types. A. S. A. Jeffrey. In Proc. IEEE Logic in Computer Science. IEEE Press. 2001. pp. 323-333. (PDF)

  • Authenticity by Typing for Security Protocols. A. D. Gordon and A. S. A. Jeffrey. In Proc. IEEE Computer Security Foundations Workshop. IEEE Press. 2001. pp. 145-159. Full version appeared in J. Computer Security 11(4). (PDF)

  • Typing Correspondence Assertions for Communication Protocols. A. D. Gordon and A. S. A. Jeffrey. In Proc. Mathematical Foundations of Programming Semantics. Elsevier. 2001. Full version appeared in Theoretical Computer Science 300. (PDF)

  • A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names. A. S. A. Jeffrey and J. Rathke. In Proc. IEEE Logic in Computer Science. IEEE Press. 2000. pp. 311-321. Full version appeared in Theoretical Computer Science 323. (PDF)

  • A Language-Based Approach to Programmable Networks. I. Wakeman, A. S. A. Jeffrey and T. Owen. In Proc. IEEE Open Architectures and Network Programming. IEEE Press. 2000. pp. 128-138. Full version appeared in Computer Networks and ISDN Systems 36(1). (PDF)

  • A Distributed Object Calculus. A. S. A. Jeffrey. In Proc. Foundations of Object Oriented Languages. 2000. (PDF)

  • A Fully Abstract Semantics for a Nondeterministic Functional Language with Monadic Types. A. S. A. Jeffrey. In Theoretical Computer Science. vol. 228. 1999. pp. 105-150. (PDF)

  • A Theory of Weak Bisimulation for Core CML. W. Ferreira, M. Hennessy and A. S. A. Jeffrey. In J. Functional Programming. 8 (5). 1998. pp. 447-491. (PDF)

  • Compilation of Higher-Order Languages in Graphical Form. R. Schweimeier and A. S. A. Jeffrey. In Proc. Mathemtical Foundations of Programming Semantics. Elsevier. 1999. (PDF)

  • Towards a Theory of Bisimulation for Local Names. A. S. A. Jeffrey and J. Rathke. In Proc. IEEE Logic in Computer Science. IEEE Press. 1999. pp. 56--66. (PDF)

  • Semantics for Core Concurrent ML Using Computation Types. A. S. A. Jeffrey. In Proc. Higher Order Operational Techniques in Semantics. Cambridge University Press. 1997. pp. 55-89. (PDF)

  • A Theory of Weak Bisimulation for Core CML. W. Ferreira, M. Hennessy and A.S.A. Jeffrey. In Proc. ACM Int. Conf. Functional Programming. ACM Press. 1996. pp. 201-212. Full version has appeared in J. Functional Programming 8(5).

  • A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types. A. S. A. Jeffrey. In Proc. IEEE Logic in Computer Science. IEEE Press. 1995. pp. 255--264. (PDF)

  • A Fully Abstract Semantics for a Nondeterministic Functional Language with Monadic Types. A. S. A. Jeffrey. In Proc. Mathematical Foundations of Programming Semantics. Elsevier. 1995. Full version has appeared in Theoretical Computer Science 228. (PDF)

  • A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours. L. Aceto and A. S. A. Jeffrey. In Theoretical Computer Science. vol. 152. 1995. pp. 251--268. (PDF)

  • Allegories of Circuits. C. Brown and A. S. A. Jeffrey. In Proc. Logical Foundations of Computer Science. Springer-Verlag. 1994. pp. 56-68. (PDF)

  • A Fully Abstract Semantics for Concurrent Graph Reduction. A. S. A. Jeffrey. In Proc. IEEE Logic in Computer Science. IEEE Press. 1994. pp. 82-91. (PDF)

  • A Chemical Abstract Machine for Graph Reduction. A. S. A. Jeffrey. In Proc. Mathematical Foundations of Programming Semantics. Springer-Verlag. 1993. pp. 293-303. (PDF)

  • Translating Timed Process Algebra into Prioritized Process Algebra. A. S. A. Jeffrey. In Proc. Formal Techniques in Real-Time and Fault-Tolerant systems. Springer-Verlag. 1992. pp. 493-506.

  • Abstract Timed Observation and Process Algebra. A. S. A. Jeffrey. In Proc. Concur. Springer-Verlag. 1991. pp. 332--345.

  • A Linear Time Process Algebra. A. S. A. Jeffrey. In Proc. Computer Aided Verification. Springer-Verlag. 1991. pp. 432--442.

Other Publications

  • Extensible protocol validation. L. E. Menten, A. S. A. Jeffrey and T. B. Reddington. U. S. Patent 8356332. 2013.

  • Dynamic Information Flow Analysis for Featherweight JavaScript. T. H. Austin, T. Disney, C. Flanagan and A. S. A. Jeffrey. U. C. Santa Cruz. UCSC-SOE-11-19. Technical Report. 2011. (PDF)

  • Robin Milner 1934-2010; Concurrency: Interaction, Bisimulation, Naming. A. S. A. Jeffrey. Presentation at ACM Principles of Programming Languages session in honour of Robin Milner. 2011. (PDF)

  • Domain Certificates in the Session Initiation Protocol (SIP). V. Gurbani, S. Lawrence and A. Jeffrey. IETF RFC 5922. 2010.

  • Combining the Typed Lambda-Calculus with CCS. In Proof, Language and Interaction: Essays in Honour of Robin Milner. W. Ferreira, M. Hennessy and A. S. A. Jeffrey. Editted by G. Plotkin and C. Stirling and M. Tofte. MIT Press. 2000. (PDF)

  • Flow Graphs and Semantics of Programs. A. S. A. Jeffrey. CTI, DePaul University. 98-004. Technical Report. 1998. (PDF)

  • A Core Data and Behaviour Language for E-LOTOS. A. S. A. Jeffrey. 1996. Input document to ISO SC21 Kansas meeting. (PDF)

  • E-LOTOS Core Language. A. S. A. Jeffrey and G. Leduc. 1996. Output document from ISO SC21 Kansas meeting. (PDF)

  • Fontinst: Font Installation Software for TeX. A. S. A. Jeffrey, et al. 1996. (PDF)

  • LaTeX2e for Authors. J. Brahms, D. Carlisle, A. S. A. Jeffrey, F. Mittelbach, C. Rowley and and R. Schöpf. The LaTeX3 Project. 1995. (PDF)

  • LaTeX2e for Class and Package Writers. J. Brahms, D. Carlisle, A. S. A. Jeffrey, F. Mittelbach, C. Rowley and and R. Schöpf. The LaTeX3 Project. 1995. (PDF)

  • Semantics for a Fragment of LOTOS with Functional Data and Abstract Datatypes. In Revised Working Draft on Enhancements to LOTOS (v3). A. S. A. Jeffrey. International Standards Organization. 1995. (PDF)

  • Towards a Proposal for Datatypes in E-LOTOS. In Revised Working Draft on Enhancements to LOTOS (v2). A. S. A. Jeffrey, H. Garavel, G. Leduc, C. Pecheur and M. Sighireanu. International Standards Organization. 1995. (PDF)

  • PostScript Fonts in LaTeX. A. S. A. Jeffrey. In Proc. TeX Users Group AGM. 1994. pp. 263--268. (PDF)

  • A Comparison of Additivity Axioms in Timed Transition Systems. A. S. A. Jeffrey, S. A. Schneider and F. Vaandrager. University of Sussex. 11/93. Computer Science Technical Report. 1993. (PDF)

  • A Fully Abstract Semantics for Concurrent Graph Reduction. A. S. A. Jeffrey. University of Sussex. 12/93. Computer Science Technical Report. 1993. (PDF)

  • A PostScript Font Installation Package Written in TeX. A. S. A. Jeffrey. In Proc. TeX Users Group AGM. 1993. pp. 285--292. (PDF)

  • A typed, prioritized process algebra. A. S. A. Jeffrey. University of Sussex. 13/93. Computer Science Technical Report. 1993. (PDF)

  • Observation Spaces and Timed Processes. A. S. A. Jeffrey. D.Phil thesis. Oxford University. 1992.

Co-authors

Conferences and workshops

Projects

Software

  • WIfL: a Web Interface Language (2012-13).

  • Agda: a dependently typed programming language and proof assistant.

    • JavaScript back end (2011).

    • agda-frp-js: Functional Reactive Programming for Agda, compiling to JavaScript (2011).

    • agda-frp-ltl: Model of Functional Reactive Programming, typed using Linear-Time Temporal Logic (2011).

    • agda-assoc-free: Difference lists, which form a monoid up to definitional equality, used to define normalization by evaluation for the simply typed lambda-calculus (2011).

    • agda-web-semantic: Semantic Web libraries for Agda, constructing a symmetric monoidal category from a description logic (2011).

    • agda-system-io: I/O libraries for Agda with semantics as a lax braided monoidal category (2010-11).

  • Cryptyc: A type checker for cryptographic protocols (2001-04).

  • Hobbes: An interpreter for an object-oriented language with formal semantics (2003).

  • Premon: An applet which draws flow graphs from program texts (1997).

  • Fontinst: Font installation software for TeX (1993-97).

  • LaTeX: A document preparation system (1992-96).

Valid XHTML + RDFa Valid CSS3 Copyright © 2000-2004 Alan Jeffrey; 2004-2014 Alcatel-Lucent.
Edited 31 March 2014.