Talks

• 2011
  • NEXCEL, a Deductive Spreadsheet, Qatar Foundation Annual Research Forum 2011 – QFARF'11, Doha, Qatar, 20 November 2011.NPRP, NEXCEL, Productivity applications, Spreadsheet paradigm, Deductive reasoning, Usability
  • QWeSST: a Language for Type-Safe Web Programming, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, 2 August 2011.Programming languages, web service, webapp, safety, parallelism, SOS, data flow, security
  • QWeSST: a Language for Type-Safe Web Programming, Microsoft Research, Cambridge, UK, 19 July 2011.Programming languages, web service, webapp, safety, parallelism, SOS, data flow, security
  • Getting CS Undergraduates to Communicate Effectively, 16th Annual AMC Conference on Innovation and Technology in Computer Science Education – ITiCSE'11, Darmstadt, Germany, 29 June 2011.CS education, writing, communication
  • Discovering Logic through Comics, 16th Annual AMC Conference on Innovation and Technology in Computer Science Education – ITiCSE'11, Darmstadt, Germany, 27 June 2011.CS education, logic, freshman, first year
  • Breaking and Fixing Public-Key Kerberos, King Abdullah University of Science and Technology — KAUST, Thuwal, Saudi Arabia, 9 May 2011.PKINIT, Kerberos, security, specification, attack, verfication
• 2010
  • Ripple: Effective Programming for Large Distributed Ensembles, Qatar Foundation Annual Research Forum 2010 – QFARF'10, Doha, Qatar, 12 December 2010.Ripple, Claytronics, programmable matter, MSR, multiset rewriting
  • Hot topics in Computer Security, Andrew's Leap, Pittsburgh, PA, 30 June 2010.Security; Qatar
  • Getting CS Undergraduates to Write, The 2010 Communication Symposium at Carnegie Mellon University: Literacy in Context – CS'10, 22 June 2010.CS education; Writing in CS; Presentations; Communication skills
  • On Teaching Programming Languages Using a Wiki, 3rd Conference on ICT in Education, Doha, Qatar, 27 March 2010.CS education; wiki; participatory learning
• 2009
  • Relating State-Based and Process-Based Concurrency through Linear Logic, Laboratoire d'Informatique, École Polytechnique, Palaiseau, France, 17 September 2009.Multiset rewriting; MSR; Linear logic; process algebra
• 2008
  • The other side of the coin: Applications of Typing in Computer Security, LPAR'08 Workshop on Application of Logic in Computer Security – ALICS'08, Doha, Qatar, 22 November 2008.Security; logic; typing
  • Empirical Evaluation of the Protocol Specification Language MSR 2, 21st IEEE Computer Security Foundations Symposium – CFS'08, Port Jefferson, NY, 23 June 2008.Multiset rewriting; MSR 2; security; protocol; specification; analysis
  • On Teaching Programming Languages Using a Wiki, The 2008 Communication Symposium at Carnegie Mellon University: Developing Disciplinary Literacy – CS'08, Pittsburgh, PA, 10 June 2008.CS education; wiki; participatory learning
  • Breaking and Fixing Public-Key Kerberos, Symposium on Recent Advances in Information Security – RAIS'08, Sharjah, UAE, 16 April 2008. Invited Speaker. Security; protocol analysis; Kerberos; PKINIT
• 2007
  • Breaking and Fixing Public-Key Kerberos, Department of Computer Science and Engineering, Qatar University, Doha, Qatar, 18 March 2007.Security; protocol analysis; Kerberos; PKINIT
• 2006
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra, Department of Mathematics, University of Pennsylvania, Philadelphia, PA, 11 December 2006.Multiset rewriting; linear logic; process algebra; security; cut eliminiation
  • Breaking and Fixing Public-Key Kerberos, 11th Annual Asian Computing Science Conference – ASIAN'06, Tokyo, Japan, 7 December 2006.Keywords: Security; protocol analysis; Kerberos; PKINIT
  • The Kerberos Verification Project, 2nd Franco-Japanese Computer Security Workshop, Tokyo, Japan, 4 December 2006.MSR; Kerberos; security; protocol verification
  • A Spreadsheet for Everyday Symbolic Reasoning, AAAI 2006 Fall Symposium on Integrating Reasoning into Everyday Applications – EVERYDAY'06, Crystal City, VA, 14 October 2006.Deductive spreadsheet; logic programming; usability; datalog
  • Hot Topics in Computer Security, Carnegie Mellon University, Doha, Qatar, 14 September 2006.Security; Qatar
  • The Deductive Spreadsheet, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 6 July 2006.Deductive spreadsheet; Datalog; usability; logic programming
  • Breaking and Fixing Public-Key Kerberos, Sixth Workshop on Issues in the Theory of Security – WITS'06, Vienna, Austria, 25 March 2006.Security; protocol analysis; Kerberos; PKINIT
  • Breaking and Fixing Public-Key Kerberos, Department of Information and Security Engineering, George Mason University, Fairfax, VA, 28 February 2006.Security; protocol analysis; Kerberos; PKINIT
• 2005
  • Breaking and Fixing Public-Key Kerberos, Department of Information and Security Engineering, George Mason University, Fairfax, VA, 30 November 2005.Security; protocol analysis; Kerberos; PKINIT
  • Towards a Notion of Quantitative Protocol Analysis, ONR Review Meeting, Shepherdstown, WV, 24 August 2005.Security; protocol analysis; denial of service; DoS
  • An Encapsulated Authentication Logic for Reasoning about Key Distribution Protocols, ONR Review Meeting, Shepherdstown, WV, 23 August 2005.Security; protocol analysis; authentication; secrecy; key distribution; Kerberos
  • Towards a Notion of Quantitative Protocol Analysis, Workshop on the Link between Formal and Computational Models, Paris, France, 23 June 2005.Security; protocol analysis; denial of service; DoS
  • An Encapsulated Authentication Logic for Reasoning about Key Distribution Protocols, 18th Computer Security Foundations Workshop – CSFW'05, Aix-en-Provence, France, 20 June 2005.Security; protocol analysis; authentication; secrecy; Kerberos
  • An Encapsulated Authentication Logic for Reasoning about Key Distribution Protocols, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 10 June 2005.Security; protocol analysis; authentication; secrecy; Kerberos
  • Specifying Kerberos 5 Cross-Realm Authentication, Protocol eXchange Seminar – PX, CISR, Naval Postgraduate School, Monterey, CA, 1 February 2005.Security; protocol analysis; Kerberos
  • Deriving Key Distribution Protocols and their Security Properties, Department of Mathematics, Tulane University, New Orleans, LA, 21 January 2005.Security; protocol analysis; authentication; security; key distribution; Kerberos
• 2004
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra, Department of Mathematics, Tulane University, New Orleans, LA, 8 October 2004.Multiset rewriting; MSR; process algebra; Petri nets; linear logic
  • Maude Implementation of MSR, ONR Workshop on Interoperability, Pervasive Computing, and Security, Savannah, GA, 1 October 2004.MSR 2; Maude; implementation
  • Maude Implementation of MSR, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 21 September 2004.MSR 2; Maude; implementation
  • Fine-Grained MSR Specifications for Quantitative Security Analysis , DIMACS Workshop on Security Analysis of Protocols, Piscataway, NJ, 9 June 2004.Security; protocol analysis; MSR; quantitative; denial of service; DoS
  • MSR 3: One Year Later, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 28 May 2004.MSR 3; multiset rewriting; process algebra; linear logic
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra, 20th Workshop on Mathematical Foundations of Programming Semantics – MFPS'04, Carnegie Mellon University, Pittsburgh, PA, 25 April 2004.Multiset rewriting; process algebra; linear logic; MSR
  • Fine-Grained MSR Specifications for Quantitative Security Analysis, Fourth Workshop on Issues in the Theory of Security – WITS'04, Barcelona, Spain, 3 April 2004.Security; protocol analysis; MSR; denial of service; DoS
  • Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types, Fifth International Workshop on Rewriting Logic and its Applications – WRLA'04, Barcelona, Spain, 27 March 2004.Security; protocol analysis; MSR; Maude
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra, Dipartimento di Sistematica e Informatica, Università di Venezia, Venice, Italy, 8 March 2004.Multiset rewriting; process algebra; linear logic; MSR
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra, New Jersey Programming Languages and Systems Seminar – NJPLS, Stevens Institute of Technology, Hoboken, NJ, 27 February 2004.Multiset rewriting; process algebra; linear logic; MSR 3
  • Fine-Grained MSR Specifications for Quantitative Security Analysis, Protocol eXchange Seminar – PX, CISR, Naval Postgraduate School, Monterey, Monterey, CA, 9 February 2004.Security; protocol analysis; MSR; denial of service; DoS
• 2003
  • Verifying Confidentiality and Authentication in Kerberos 5, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 16 December 2003.Security; protocol analysis; Kerberos 5; MSR
  • Verifying Confidentiality and Authentication in Kerberos 5, 2003 International Symposium on Software Security – ISSS'03, Tokyo, Japan, 5 November 2003.Security; protocol analysis; Kerberos 5
  • MSR 3.0: the Logical Meeting Point of Multiset Rewriting and Process Algebra, 2003 International Symposium on Software Security – ISSS'03, Tokyo, Japan, 4 November 2003.Multiset rewriting; process algebra; linear logic; MSR 3
  • MSR 3.0: the Logical Meeting Point of Multiset Rewriting and Process Algebra, Workshop on Formal on Formal Methods in Security Engineering – FMSE'03, Washington, DC, 30 October 2003. Invited Speaker. Multiset rewriting; process algebra; linear logic; MSR 3
  • Logical Foundations of Multiset Rewriting, Department of Computer Science, Princeton University, Princeton, NJ, 17 October 2003.Multiset rewriting; linear logic
  • One Picture is Worth a Thousand Words, well ... a Couple Dozen Connectives, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 1 October 2003.NPATRL; GDOI; fault tree; security requirements; dependence trees
  • One Picture is Worth a Thousand Words, well ... a Couple Dozen Connectives, ONR Workshop on Interoperability, Pervasive Computing, and Security, Harpers Ferry, WV, 24 September 2003.NPATRL; GDOI; fault tree; security requirements; dependence trees
  • Relating Multiset Rewriting and Process Algebra for Immediate Decryption Protocols, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 11 June 2003.Security; protocol analysis; multiset rewriting; MSR; process algebra
  • A Concurrent Logical Framework, Department of Computer Science, Stevens Institute of Technology, Hoboken, NJ, 6 May 2003.Type theory; LF; concurrency; linear logic; monad; CLF
  • Relating Multiset Rewriting and Process Algebra for Security Protocol Specification, Department of Mathematics, Tulane University, New Orleans, LA, 17 April 2003.Multiset rewriting; process algebra; linear logic; security; protocol analysis
  • Relating Multiset Rewriting and Process Algebra for Security Protocol Specification, Third Workshop on Issues in the Theory of Security – WITS'03, Warsaw, Poland, 5 April 2003.Multiset rewriting; process algebra; linear logic; security; protocol analysis
  • A Concurrent Logical Framework, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 27 February 2003.Type theory; linear logic; concurrency; monad; LF; CLF
  • MSR 3.0: the Logical Meeting Point of Multiset Rewriting and Process Algebra, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 27 February 2003.Multiset rewriting; linear logic; process algebra; MSR 3
  • Strand Spaces and Beyond, Department of Computer Science, Princeton University, Princeton, NJ, 6 February 2003.
• 2002
  • MSR by Examples, Kestrel Institute, Palo Alto, CA, 4 December 2002.Security; protocol analysis; specification; MSR 2
  • MSR by Examples, Department of Computer and Information Systems, University of Pennsylvania, Philadelphia, PA, 26 November 2002.Security; protocol analysis; specification; multiset rewriting; MSR
  • A Concurrent Logical Framework, International Symposium on Software Security – ISSS'02, Tokyo, Japan, 10 October 2002.Type theory; linear logic; concurrency; monads; LF; CLF
  • Proof-Theoretic Foundation of Compilation in Logic Programming Languages, Department of Computer Science, Princeton University, Princeton, NJ, 8 October 2002.Logic programming; proof theory; compilation; WAM
  • Solution Count for Multiset Unification with Trailing Multiset Variables, Sixteenth International Workshop on Unification – UNIF'02, Copenhagen, Denmark, 26 July 2002.Multiset rewriting; unification
  • MSR by Examples, Computer Science and Engineering Department, Indian Institute of Technology, Delhi, India, 24 April 2002.Security; protocol analysis; specification; multiset rewriting; MSR 2
  • The Wolf Within, Second Workshop on Issues in the Theory of Security – WITS'02, Portland, OR, 14 January 2002.Security; protocol specification; Dolev-Yao intruder
• 2001
  • A Specification Language for Crypto-Protocols based on Multiset Rewriting Dependent Types and Subsorting, ICLP 2001 workshop on Specification, Analysis and Validation for Emerging Technologies in Computational Logic – SAVE'01, Paphos, Cyprus, 1 December 2001.Security; protocol analysis; specification; multiset rewriting; MSR 2
  • Expressing Type-Flaw Attacks in a Strongly-Typed Language, Second Workshop on Foundations for Secure/Survivable Systems and Networks, Tokyo, Japan, 27 October 2001.Security; protocola analysis; type-flaw attacks; Dolev-Yao model; MSR 2; dependent types
  • The Wolf Within, seminar on Specification and Analysis of Secure Cryptographic Protocols, Dagstuhl, Germany, 24 September 2001.Security; protocol analysis; Dolev-Yao model; MSR 2
  • Abstract Specification of Crypto-Protocols and their Attack Models in MSR, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, 6 August 2001.Security; protocol analysis; Dolev-Yao model; MSR 2
  • Automated Intruder Generation, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 18 July 2001.Security; protocol analysis; Dolev-Yao model; MSR 2
  • The Dolev-Yao Intruder is the Most Powerful Attacker, 16th Annual IEEE Symposium on Logic in Computer Science – LICS'01, Boston, MA, 18 June 2001.Security; protocol analyis; Dolev-Yao model; MSR 2
  • Typed MSR: Syntax and Examples, First International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security – MMM'01, St. Petersburg, Russia, 22 May 2001.Security; protocol analysis; multiset rewriting; MSR 2
  • MSR, a Framework for Security Protocols and their Meta-Theory, Protocol eXchange Seminar – PX, Department of Computer Science, University of Maryland, Baltimore County, Baltimore, MD, 23 April 2001.Security; protocol analysis; MSR 2
  • A (Linear) Spine Calculus, Seminar on Semantic Foundations of Proof-search, Dagstuhl, Germany, 4 April 2001.Type theory; linear logic; higher-order unification
  • MSR by Examples, Workshop on Programming and Programming Languages – PPL'01, Kameoka, Japan, 21 March 2001. Invited speaker. Security; protocol analysis; specification; multiset rewriting; MSR 2
  • MSR, a Framework for Security Protocols and their Meta-Theory, Graduate School of Information Science, Japan Advanced Institute of Science and Technology — JAIST, Kanazawa, Japan, 15 March 2001.Security; protocol analyisis; specification; multiset rewriting; MSR 2
  • MSR, a Framework for Security Protocols and their Meta-Theory, Department of Information Science, University of Tokyo, Tokyo, Japan, 12 March 2001.Security; protocol analyisis; specification; multiset rewriting; MSR 2
  • MSR, a Framework for Security Protocols and their Meta-Theory, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 2 February 2001.Security; protocol analyisis; specification; multiset rewriting; MSR 2
• 2000
  • A Flexible Methodology for Specifying Security Protocols, Seminar on Security through Analysis and Verification, Dagstuhl, Germany, 15 December 2000.Security; protocol analysis; MSR; specification
  • Relating Strands and Multiset Rewriting Specification of Security Protocols, International School on Foundations of Security Analysis and Design – FOSAD'00, Bertinoro, Italy, 26 September 2000.Security; protocol analysis; strand spaces; MSR; multiset rewriting
  • Multiset Rewriting Specification of Security Protocols, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology – MFSCIT'01, Cork, Ireland, 21 July 2000.Security; protocol specification; MSR
  • A Calculus of Macro-Events: Progress Report, 7th International Workshop on Temporal Representation and Reasoning – TIME'00, Cape Breton, NS, Canada, 7 July 2000.Temporal reasoning; event calculus
  • Relating Strands and Multiset Rewriting for Security Protocol Analysis, 13th Computer Security Foundations Workshop – CSFW'00, Cambridge, UK, 3 July 2000.Security; protocol analysis; strand spaces; MSR
  • Security Protocol Specification with Strands and Multiset Rewriting, Dipartimento di Informatica e Matematica, University of Udine, Udine, Italy, 30 June 2000.Security; protocol specification; strand spaces; MSR
  • Are Transition-Based Systems beyond the Reach of Logical Frameworks?, NSF-JSPS Cooperative Science Program "Logical Methods for Formal Verification of Software" kickoff meeting, Stanford University, Stanford, CA, 14 March 2000.State-based systems; transition; logic; logical framework; LLF
  • Formalizing Strands, Strand Meeting, University of Maryland, Baltimore County, Baltimore, MD, 3 February 2000.Security; protocol specification; strand spaces
• 1999
  • Explicit Substitutions for Linear Logical Frameworks: Preliminary Results, Workshop on Logical Frameworks and Meta-languages – LFM'99, Paris, France, 28 September 1999.Linear logic; explicit substitutions; logical frameworks; LLF
  • Reasoning about State in a Linear Logical Framework, Naval Research Laboratory, Washington, DC, 23 April 1999.LLF; linear logic; state
• 1998
  • The Linear Logical Framework LLF, Département d'Informatique, Université Laval, Québec, Canada, 16 October 1998.Logical frameworks; linear logic; LLF
  • A Modular Analysis of the Event Calculus with Modalities, Connectives, Quantifiers, and Preconditions, Department of Computing and Mathematics, Manchester Metropolitan University, Manchester, UK, 18 June 1998.Temporal reasoning; event calculus
  • Proof-Theoretic Foundation of Compilation in Logic Programming Languages, 1998 Joint International Conference and Symposium on Logic Programming – JICSLP'98, Manchester, UK, 17 June 1998.logic programming; compilation; WAM; linear logic
  • The Linear Logical Framework LLF, Seventh Annual Workshop on Logic, language and Computation, CSLI, Stanford, CA, 29 May 1998.Logical framework; linear logic; LLF
  • Event Calculus with Explicit Quantifiers, Fifth International Workshop on Temporal Representation and Reasoning – TIME'98, Sanibel Island, FL, 17 May 1998.Temporal reasoning; event calculus
  • Proof-Theoretic Foundation of Compilation in Logic Programming Languages, Department of Computer and Information Systems, University of Pennsylvania, Philadelphia, PA, 4 May 1998.Logic programming; compilation; linear logic; WAM
  • The Linear Logical Framework LLF, Linear Logic Workshop, CIRM, Marseille, France, 7 April 1998.
  • Proof-Theoretic Foundation of Compilation in Logic Programming Languages, Computer Science Laboratory, SRI International, Menlo Park, CA, 5 February 1998.Logic programming; compilation; linear logic; WAM
• 1997
  • A Linear Logical Framework, Research Institute for Mathematical Sciences, University of Kyoto, Kyoto, Japan, 2 June 1997.Logical frameworks; linear type theory; LLF
  • Modal Event Calculi with Preconditions, Fourth International Workshop on Temporal Representation and Reasoning – TIME'97, Daytona Beach, FL, 10 May 1997.Temporal reasoning; event calculus
  • A Linear Logical Framework, School of Computer Science, Telecommunications and Information Systems, DePaul University, Chicago, IL, 2 May 1997.Logical frameworks; linear type theory; LLF
  • A Linear Logical Framework, Department of Computer Science and Engineering, Pennsylvania State University, State College, PA, 17 February 1997.
  • A Linear Logical Framework, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, 27 January 1997.Logical frameworks; linear type theory; LLF
• 1996
  • A Linear Logical Framework, Dipartimento di Informatica e Matematica, University of Udine, Udine Italy, 23 October 1996.Logical frameworks; linear type theory; LLF
  • A Linear Logical Framework, 11th Annual IEEE Symposium on Logic in Computer Science – LICS'96, New Brunswick, NJ, 28 July 1996.Logical frameworks; linear type theory; LLF
  • A Linear Logical Framework, CRIN-LORIA, Nancy, France, 4 July 1996.Logical frameworks; linear type theory; LLF
  • Efficient Resource Management for Linear Logic Proof Search, International Workshop on Extensions of Logic Programming – ELP'96, Leipzig, Germany, 29 March 1996.Linear logic; context management
  • A Linear Logical Framework, Ph.D. thesis defense, Milano, Italy, 6 February 1996.Logical frameworks; linear type theory; LLF
• 1995
  • Efficient Resource Management for Linear Logic Proof Search, Dipartimento di Informatica e Matematica, University of Udine, Udine, Italy, 16 November 1995.Linear logic; context management
  • Petri Nets and Linear Logic: a Case Study for Logic Programming, Joint Conference on Declarative Programming – GULP-PRODE'95, Marina di Vietri, Italy, 12 September 1995.Linear logic; representation; logic programming; Petri nets
• 1994
  • Modal Event Calculus, International Logic Programming Symposium 1994 – ILPS'94, Ithaca, NY, 17 November 1994.Temporal reasoning; event calculus
  • Lollipops taste of Vanilla too, Workshop on Proof-theoretical Extensions of Logic Programming – ELP'94, Santa Margherita Ligure, Italy, 18 June 1994.Linear logic; meta-interpreters; logic programming
• 1993
  • A WAM Implementation for the Logic Meta Programming Language 'Log, 8th Italian Conference on Logic Programming – GULP'93, Gizzeria Lido, Italy, 16 June 1993.Logic programming; meta-programming; 'Log; WAM
  • Expression and Enforcement of Dynamic Integrity Constraints, First Italian Conference on Advanced Database Systems – SEBD'93, Gizzeria Lido, Italy, 15 June 1993.Database; integrity constraints
  • On the Non-Monotonic Behavior of the Event Calculus for Deriving Maximal Time Intervals, International Conference on Numerical Analysis with Automatic Result Verification, Lafayette, LA, 26 February 1993.Temporal reasoning; event calculus
• 1992
  • A WAM Implementation for the Meta-Logic Programming Language 'Log, Master's thesis defense, Department of Computer Science, University of Houston, Houston, TX, 24 July 1992.Logic programming; meta-programming; 'Log; WAM
• 1991
  • Una Proposta per l'Introduzione di Capacità di Meta-Rappresentazione in un Linguaggio di Programmazione Logica, Bachelor thesis defense, Dipartimento di Informatica e Matematica, University of Udine, Udine, Italy, 7 March 1991. (In Italian). Logic programming; meta-programming; 'Log