Magic Trixie's Dad

Alan Jeffrey

Software EngineerRoblox

Software

Current project

Roblox Game Engine, focusing on the Luau scripting language.

Previous projects

Servo: a parallel browser engine (2015-20).

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).

Research

Bibliographies

BibTeX

DBLP

Google Scholar

Refereed Papers

B. Greenman, A. S. A. Jeffrey, S. Krishnamurthi and M. Shah, Type Error Telemetry at Scale, in The Art, Science, and Engineering of Programming, 2024.

L. Brown, A. Friesen and A. S. A. Jeffrey, Goals of the Luau Type System, Two Years On, in Proc. Human Aspects of Types and Reasoning Assistants, 2023.

A. S. A. Jeffrey, J. Riely, M. Batty, S. Cooksey, I. Kaysin and A. Podkopaev, The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency, in Proc. ACM Int. Conf. Principles of Programming Languages, 2022.

L. Brown, A. Friesen and A. S. A. Jeffrey, Goals of the Luau Type System, in Proc. Human Aspects of Types and Reasoning Assistants, 2021.

R. Jagadeesan, A. S. A. Jeffrey and J. Riely, Pomsets with Preconditions: A Simple Model of Relaxed Memory, in Proc. ACM OOPSLA, 2020.

A. S. A. Jeffrey and J. Riely, On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory, in Proc. IEEE Logic in Computer Science, 2016.

A. S. A. Jeffrey and T. Van Cutsem, Functional Reactive Programming with nothing but Promises: Implementing Push/Pull FRP using JavaScript Promises, in Proc. Workshop on Reactive and Event-based Languages and Systems, 2015.

A. S. A. Jeffrey, Functional Reactive Types, in Proc. EACSL Computer Science Logic / IEEE Logic in Computer Science, 2014.

M. Goto, R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J Riely, An Extensible Approach to Session Polymorphism, in Math. Struct. in Comp. Science, 2014.

A. S. A. Jeffrey, Functional Reactive Programming with Liveness Guarantees, in Proc. ACM Int. Conf. Functional Programming, 2013.

P. J. Danielsen and A. S. A. Jeffrey, Validation and Interactivity of Web API Documentation, in Proc. IEEE Int. Conf. Web Services, 2013.

A. S. A. Jeffrey, Causality For Free!: Parametricity Implies Causality for Functional Reactive Programs, in Proc. ACM Workshop Programming Languages meets Program Verification, 2013.

A. S. A. Jeffrey, Dependently Typed Web Client Applications: FRP in Agda in HTML5, in Proc. Practical Aspects of Declarative Languages, 2013.

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

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

A. S. A. Jeffrey and J. Rathke, The Lax Braided Structure of Streaming I/O, in Proc. Conf. Computer Science Logic, 2011.

A. S. A. Jeffrey and P. F. Patel-Schneider, Integrity Constraints for Linked Data, in Proc. Int. Workshop Description Logics, 2011.

R. Jagadeesan, A. Jeffrey, C. Pitcher and J. Riely, Confidential Safety via Correspondence Assertions, in Proc. Workshop Foundations of Security and Privacy, 2010.

R. Jagadeesan, A. Jeffrey, C. Pitcher and J. Riely, Towards a Theory of Accountability and Audit, in Proc. European Symp. Research in Computer Security, 2009.

A. S. A. Jeffrey and T. Samak, Model Checking Firewall Policy Configurations, in Proc IEEE Int. Symp. Policies for Distributed Systems and Networks, 2009.

M. Benedikt, A. S. A. Jeffrey and R. Ley-Wild, Stream Firewalling of XML Constraints, in Proc. ACM SIGMOD Int. Conf. Management of Data, 2008.

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

M. Benedikt and A. S. A. Jeffrey, Efficient and Expressive Tree Filters, in Proc. Foundations of Software Technology and Theoretical Computer Science, 2007.

A. S. A. Jeffrey and J. Rathke, Full Abstraction for Polymorphic Pi-Calculus, in Theoretical Computer Science, 2008.

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

C. Haack and A. S. A. Jeffrey, Pattern-Matching Spi-Calculus, in Information and Computation, 2006.

R. Jagadeesan, A. S. A. Jeffrey and J. Riely, Typed Parametric Polymorphism for Aspects, in Science of Computer Programming, 2006.

R. Jagadeesan, A. S. A. Jeffrey, C. Pitcher and J. Riely, Lambda-RBAC: Programming with Role-Based Access Control, in Proc. Int. Colloq. Automata, Languages and Programming, 2006.

A. D. Gordon and A. S. A. Jeffrey, Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus, in Proc. Concur, 2005.

C. Haack and A. S. A. Jeffrey, Timed Spi-calculus with Types for Secrecy and Authenticity, in Proc. Concur, 2005.

A. S. A. Jeffrey and J. Rathke, Contextual Equivalence for Higher-Order Pi-Calculus Revisited, in Logical Methods in Computer Science, 2005.

A. S. A. Jeffrey and J. Rathke, Java Jr.: Fully Abstract Trace Semantics for a Core Java Language, in Proc. European Symposium on Programming, 2005.

A. S. A. Jeffrey and J. Rathke, Full Abstraction for Polymorphic Pi-Calculus, in Proc. Foundations of Software Science and Computation Structures, 2005.

C. Haack and A. S. A. Jeffrey, Pattern-Matching Spi-Calculus, in Proc. IFIP WG 1.7 Workshop on Formal Aspects in Security and Trust, 2004.

A. S. A. Jeffrey and J. Rathke, A Fully Abstract May Testing Semantics for Concurrent Objects, in Theoretical Computer Science, 2005.

G. Bruns, R. Jagadeesan, A. S. A. Jeffrey and J. Riely, muABC: A Minimal Aspect Calculus, in Proc. Concur, 2004.

A. D. Gordon and A. S. A. Jeffrey, Types and Effects for Asymmetric Cryptographic Protocols, in J. Computer Security, 2004.

A. S. A. Jeffrey and J. Rathke, A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names, in Theoretical Computer Science, 2004.

A. D. Gordon and A. S. A. Jeffrey, Authenticity by Typing for Security Protocols, in J. Computer Security, 2003.

A. D. Gordon and A. S. A. Jeffrey, Typing Correspondence Assertions for Communication Protocols, in Theoretical Computer Science, 2003.

I. Wakeman, A. S. A. Jeffrey, T. Owen and D. Pepper, SafetyNet: A Language-Based Approach to Programmable Networks, in Computer Networks and ISDN Systems, 2001.

R. Jagadeesan, A. S. A. Jeffrey and J. Riely, A Calculus of Untyped Aspect-Oriented Programs, in Proc. European Conf. Object-Oriented Programming, 2003.

A. S. A. Jeffrey and J. Rathke, Contextual Equivalence for Higher-Order Pi-Calculus Revisited, in Proc. Mathematical Foundations of Programming Semantics, 2003.

A. D. Gordon and A. S. A. Jeffrey, Types and Effects for Asymmetric Cryptographic Protocols, in Proc. IEEE Computer Security Foundations Workshop, 2002.

A. D. Gordon and A. S. A. Jeffrey, Typing One-to-One and One-to-Many Correspondences in Security Protocols, in Proc. Int. Software Security Symp., 2002.

A. S. A. Jeffrey and J. Rathke, A Fully Abstract May Testing Semantics for Concurrent Objects, in Proc. IEEE Logic In Computer Science, 2002.

A. S. A. Jeffrey, A Symbolic Labelled Transition System for Coinductive Subtyping of F-mu-sub Types, in Proc. IEEE Logic in Computer Science, 2001.

A. D. Gordon and A. S. A. Jeffrey, Authenticity by Typing for Security Protocols, in Proc. IEEE Computer Security Foundations Workshop, 2001.

A. D. Gordon and A. S. A. Jeffrey, Typing Correspondence Assertions for Communication Protocols, in Proc. Mathematical Foundations of Programming Semantics, 2001.

A. S. A. Jeffrey and J. Rathke, A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names, in Proc. IEEE Logic in Computer Science, 2000.

I. Wakeman, A. S. A. Jeffrey and T. Owen, A Language-Based Approach to Programmable Networks, in Proc. IEEE Open Architectures and Network Programming, 2000.

A. S. A. Jeffrey, A Distributed Object Calculus, in Proc. Foundations of Object Oriented Languages, 2000.

A. S. A. Jeffrey, A Fully Abstract Semantics for a Nondeterministic Functional Language with Monadic Types, in Theoretical Computer Science, 1999.

W. Ferreira, M. Hennessy and A. S. A. Jeffrey, A Theory of Weak Bisimulation for Core CML, in J. Functional Programming, 1998.

R. Schweimeier and A. S. A. Jeffrey, Compilation of Higher-Order Languages in Graphical Form, in Proc. Mathemtical Foundations of Programming Semantics, 1999.

A. S. A. Jeffrey and J. Rathke, Towards a Theory of Bisimulation for Local Names, in Proc. IEEE Logic in Computer Science, 1999.

A. S. A. Jeffrey, Semantics for Core Concurrent ML Using Computation Types, in Proc. Higher Order Operational Techniques in Semantics, 1997.

W. Ferreira, M. Hennessy and A.S.A. Jeffrey, A Theory of Weak Bisimulation for Core CML, in Proc. ACM Int. Conf. Functional Programming, 1996.

A. S. A. Jeffrey, A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types, in Proc. IEEE Logic in Computer Science, 1995.

A. S. A. Jeffrey, A Fully Abstract Semantics for a Nondeterministic Functional Language with Monadic Types, in Proc. Mathematical Foundations of Programming Semantics, 1995.

L. Aceto and A. S. A. Jeffrey, A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours, in Theoretical Computer Science, 1995.

C. Brown and A. S. A. Jeffrey, Allegories of Circuits, in Proc. Logical Foundations of Computer Science, 1994.

A. S. A. Jeffrey, A Fully Abstract Semantics for Concurrent Graph Reduction, in Proc. IEEE Logic in Computer Science, 1994.

A. S. A. Jeffrey, A Chemical Abstract Machine for Graph Reduction, in Proc. Mathematical Foundations of Programming Semantics, 1993.

A. S. A. Jeffrey, Translating Timed Process Algebra into Prioritized Process Algebra, in Proc. Formal Techniques in Real-Time and Fault-Tolerant systems, 1992.

A. S. A. Jeffrey, Abstract Timed Observation and Process Algebra, in Proc. Concur, 1991.

A. S. A. Jeffrey, A Linear Time Process Algebra, in Proc. Computer Aided Verification, 1991.

Other Publications

A. S. A. Jeffrey, Semantic Subtyping in Luau, Roblox Technical Blog, 2022.

A. S. A. Jeffrey, Servo, Spectre and the interfaces between browser, operating system and hardware, 2019.

A. S. A. Jeffrey, Josephine: Using JavaScript to safely manage the lifetimes of Rust data, arXiv:1807.00067 [cs.PL], 2018.

A. S. A. Jeffrey and J. Riely, Event Structures and Refinement for Relaxed Memory, Presented at the Cambridge memory model meeting, 2014.

C. G. Brewster and A. S. A. Jeffrey, A Model of Navigation History, arXiv:1608.05444 [cs.SE], 2016.

A. S. A. Jeffrey, Tools for Writing a Research Paper, Research methods class at UIC, 2015.

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

T. H. Austin, T. Disney, C. Flanagan and A. S. A. Jeffrey, Dynamic Information Flow Analysis for Featherweight JavaScript, 2011.

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

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

W. Ferreira, M. Hennessy and A. S. A. Jeffrey, Combining the Typed Lambda-Calculus with CCS, in Proof, Language and Interaction: Essays in Honour of Robin Milner, 2000.

A. S. A. Jeffrey, Flow Graphs and Semantics of Programs, 1998.

A. S. A. Jeffrey and others, Fontinst: Font Installation Software for TeX, 1996.

A. S. A. Jeffrey, A Core Data and Behaviour Language for E-LOTOS, 1996.

A. S. A. Jeffrey and G. Leduc, E-LOTOS Core Language, 1996.

A. S. A. Jeffrey, Semantics for a Fragment of LOTOS with Functional Data and Abstract Datatypes, in Revised Working Draft on Enhancements to LOTOS (v3), 1995.

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

J. Brahms, D. Carlisle, A. S. A. Jeffrey, F. Mittelbach, C. Rowley and and R. Sch\"opf, LaTeX2e for Authors, 1995.

J. Brahms, D. Carlisle, A. S. A. Jeffrey, F. Mittelbach, C. Rowley and and R. Sch\"opf, LaTeX2e for Class and Package Writers, 1995.

A. S. A. Jeffrey, PostScript Fonts in LaTeX, in Proc. TeX Users Group AGM, 1994.

A. S. A. Jeffrey, A PostScript Font Installation Package Written in TeX, in Proc. TeX Users Group AGM, 1993.

A. S. A. Jeffrey, A typed, prioritized process algebra, 1993.

A. S. A. Jeffrey, A Fully Abstract Semantics for Concurrent Graph Reduction, 1993.

A. S. A. Jeffrey, S. A. Schneider and F. Vaandrager, A Comparison of Additivity Axioms in Timed Transition Systems, 1993.

A. S. A. Jeffrey, Observation Spaces and Timed Processes, 1992.

Co-authors

Luca Aceto, School of Computer Science, Reykjavik University.

Mark Batty, School of Computing, University of Kent.

Michael Benedikt, Computing Laboratory, Oxford University.

Lily Brown, Roblox.

Glenn Bruns, Bell Labs, Alcatel-Lucent.

Simon Cooksy, School of Computing, University of Kent.

Peter J. Danielsen, Bell Labs, Alcatel-Lucent.

Andy Friesen, Roblox.

Andrew D. Gordon, Microsoft Research.

Vijay Gurbani, Bell Labs, Alcatel-Lucent.

Matthew Goto, School of Computing, DePaul University.

Christian Haack, Security of Systems Group, University of Nijmegen.

Matthew Hennessy, Computer Science Department, Trinity College Dubdivn.

Radha Jagadeesan, School of Computing, DePaul University.

Ilya Kaysin, JetBrains Research and University of Cambridge.

Corin Pitcher, School of Computing, DePaul University.

Ruy Ley-Wild, School of Computer Science, Carnegie Mellon University.

Peter F. Patel-Schneider, Bell Labs, Alcatel-Lucent.

Anton Podkopaev, JetBrains Research and Higher School of Economics.

Judivan Rathke, School of Electronics and Computer Science, University of Southampton.

James Riely, School of Computing, DePaul University.

Ralf Schweimeier, Department of Computing, City University.

Ian Wakeman, Informatics, University of Sussex.

Conferences and workshops

ACM Int. Conf. Functional Programming (ICFP) 2023: PC Member.

ACM Symp. Principles of Programming Languages (PoPL) 2023: PC member.

ACM Workshop on Reactive and Event-based Languages & Systems (REBLS) 2020-23: PC Member.

ACM Workshop on Human Aspects of Types and Reasoning Assistants (HATRA) 2022-23: PC Member.

ACM Int. Conf. Functional Programming (ICFP) 2018-21: Industrial Relations Chair.

ACM Workshop on Reactive and Event-based Languages & Systems (REBLS) 2020-21: PC Member.

ACM Workshop on Human Aspects of Types and Reasoning Assistants (HATRA) 2021: PC Member.

AAAI Workshop on Programming Languages and Interactive Entertainment (PLIE) 2021: PC Member.

ACM Symp. Principles of Programming Languages (PoPL) 2019: PC member.

Principles of Secure Compilation (PriSC) 2019: PC member.

ACM/IEEE Symp. Logic In Computer Science (LICS) 2018: PC member.

ACM Int. Conf. Functional Programming (ICFP) 2017: PC member.

Workshop on Incremental Computing (IC) 2017: PC member.

Int. Conf. Formal Techniques for Distributed Systems (FORTE) 2015: PC member.

Mathematical Foundations of Programming Semantics (MFPS) 2015: PC member.

Dependently Typed Programming (DTP) 2014: Invited speaker.

ACM Symp. Principles of Programming Languages (PoPL) 2014: PC member.

Principles, Systems and Applications of IP Telecommunications (IPTComm) 2014: PC member.

ACM Int. Conf. Functional Programming (ICFP) 2013: PC member.

IFIP Joint Int. Conf. Formal Techniques for Distributed Systems (FORTE/FMOODS) 2013: PC member.

Workshop on Foundations of Computer Security (FCS) 2013: PC member.

Principles, Systems and Applications of IP Telecommunications (IPTComm) 2013: PC member.

Workshop on Foundations of Computer Security (FCS) 2011: PC co-chair.

Principles, Systems and Applications of IP Telecommunications (IPTComm) 2011: PC member.

Principles, Systems and Applications of IP Telecommunications (IPTComm) 2010: PC member.

IFIP Int. Conf. Theoretical Computer Science (TCS) 2010: PC member.

Int. Conf. Foundations Of Software Science And Computation Structures (FoSSaCS) 2009: PC member.

EACSL Conf. Computer Science Logic (CSL) 2008: PC member.

Int. Workshop on Expressiveness in Concurrency (Express) 2008: PC member.

Int. Conf. Concurrency Theory (CONCUR) 2007: PC member.

European Symp. Programming (ESOP) 2007: PC member.

IEEE Symp. Logic In Computer Science (LICS) 2007: PC member.

Symp. Trustworthy Global Computing (TGC) 2007: PC member.

IEEE Computer Security Foundations Workshop (CSFW) 2006: PC member.

European Symp. Research In Computer Security (ESORICS) 2006: PC member.

Foundations of Aspect-Oriented Languages Workshop (FOAL) 2006: PC member.

ACM Workshop on Formal Methods in Security Engineeringm (FMSE) 2006: PC member.

Copyright © 2000-2004 Alan Jeffrey; 2004-2015 Alcatel-Lucent; 2015-2020 Mozilla Corporation; 2020-2023 Roblox. Last modified 12 December 2023.