Publications

• 2018
  • With Sharjeel Khan, Giselle Reis and Dragiša Žunić: Formalization of Automated Trading Systems in a Concurrent Linear Framework, 2018 Joint Workshop on Linearity and Trends in Linear Logic and Applications — LINEARITY'18, Oxford, UK, 7-8 July 2018. affiliated with with FCSD at FLOC 2018.
    papers/linearity18.pdf
  • With Sandra Alves: Special issue on Linearity 2014, Mathematical Structures in Computer Science — MSCS, vol. 28(5), Cambridge University Press, July 2018.
    DOI
• 2017
  • With Baljit Singh, Dmitry Evtyushkin, Jesse Elwell and Ryan Riley: On the Detection of Kernel-Level Rootkits Using Hardware Performance Counters, 12th ACM Asia Conference on Computer and Communications Security — ASIACCS'17, Abu Dhabi, UAE, 2-6 April 2017. Rootkits; Hardware Performance Counters; Intrusion Detection; Machine Learning
    papers/asiacrypt17.pdfDOI
• 2016
  • With Edmund S.L. Lam: Concurrent Logic Programming: Met and Unmet Promises, First Workshop on Applications of Logic Programming — AppLP'16 (David Warren and Annie Liu, editors), New York City, USA, 17 October 2016.
    papers/applp16.pdf
  • With Edmund S.L. Lam and Ali Elgazar: Choreographic Compilation of Decentralized Comprehension Patterns (best paper award) , 10th International Web Rule Symposium — RuleML'16 (Jose Julio Alferes, Leopoldo Bertossi and Guido Governatori, editors), 1-17, Springer LNCS 9718, Stony Brook, NY, 6-9 July 2016.
    papers/ruleml16.pdfDOIvideo
  • With Edmund S.L. Lam: Let's Unify Like Scala Pattern Matching!, 30th International Workshop on Unification — UNIF'16 (Silvio Ghilardi and Manfred Schmidt-Schauß, editors), Porto, Portugal, 26 June 2016.
    papers/unif16a.pdfby Edmund S.L. Lam
  • With Edmund S.L. Lam: Overlap and Independence in Multiset Comprehension Patterns, 30th International Workshop on Unification — UNIF'16 (Silvio Ghilardi and Manfred Schmidt-Schauß, editors), 26 June 2016.
    papers/unif16b.pdf
  • With Maribel Fernández (co-editor): Linearity 2016, Proceedings of the Fourth International Workshop on Linearity — LINEARITY'16, EPTCS, vol. 238, Porto, Portugal, 25 June 2016. ISSN: 2075-2180.Linear Logic, Proof Theory, Complexity Classes, Program Analysis, Operational Semantics, Programming Languages, Program Transformation
  • With Jesse Elwell, Ryan Riley, Nael Abu-Ghazaleh and Dmitry Ponomarev: Rethinking Memory Permissions for Protection Against Cross-Layer Attacks, ACM Transactions on Architecture and Code Optimization — TACO, vol. 12(4) (Koen De Bosschere, editor), ACM, January 2016.
    papers/taco16.pdfDOI
• 2015
  • With Edmund S.L. Lam: Modular Multiset Rewriting, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning — LPAR'15 (Martin Davis, Andrei Voronkov, Annabelle McIver and Ansgar Fehnker, editors), 1-17, Springer LNCS 9450, Suva, Fiji, 24-28 November. Rule-based programming; modularity; logic; focusing; functor; abstract data types
    papers/lpar15.pdfDOI
  • With Carsten Schürmann (co-editor): WoF 2015, Proceedings First International Workshop on Focusing — WoF'15, EPTCS, vol. 197, Suva, Fiji, 23 November 2015. ISSN: 2075-2180.Computational logic; logic programming; theorem proving; proof search; focusing
    ProceedingsDOI
  • With Edmund S.L. Lam and Ali Elgazar: Programmable Orchestration of Time-Synchronized Events Across Decentralized Android Ensembles, 11th IEEE International Conference on Wireless and Mobile Computing, Networking and Communications — WiMob'15, 659-666, IEEE Xplore Digital Library, Abu Dhabi, UAE, 19-21 October 2015. Multiset rewriting, Orchestration, Android, Time Synchronization
    papers/wimob15.pdfDOI
  • With Kaustuv Chaudhuri (co-editor): LFMTP 2015, Proceedings of the Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice — LFMTP'15, EPTCS, vol. 185, Berlin, Germany, 1 August 2015. ISSN: 2075-2180.Computer Science; Logic; Type theory; Logical frameworks; meta-language; Theorem proving; Deduction; Programming Languages
    DOI
  • With Edmund S.L. Lam: Modular Multiset Rewriting in Focused Linear Logic, Technical Report CMU-CS-15-117, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2015. Multiset Rewriting, Logic Programming, Modularity, Focused Search
    papers/cmu-cs-15-117.pdf
  • With Edmund S.L. Lam and Nabeeha Fatima Haque: Comingle: Distributed Logic Programming for Decentralized Mobile Ensembles, 17th IFIP International Conference on Coordination Models and Languages — COORDINATION'15 (Tom Holvoet and Mirko Viroli, editors), 51-66, Springer LNCS 9037, Grenoble, France, 2-4 June 2015. Multiset rewriting, mobile computation, Android, actuator, trigger, distributed system
    papers/coordination15.pdfDOIby Edmund S.L. Lam
  • With Edmund S.L. Lam: Comingle: Distributed Logic Programming for Decentralized Android Applications, Technical Report CMU-CS-15-101, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, February 2015. Multiset Rewriting, Logic Programming, Android Mobile Programming
    papers/cmu-cs-15-101.pdf
  • With Sandra Alves (co-editor): Linearity 2014, Proceedings of the Third International Workshop on Linearity — LINEARITY'14, EPTCS, vol. 176, Vienna, Austria, 13 July 2014. ISSN: 2075-2180.Linear Logic, Proof Theory, Complexity Classes, Quantum Computation, Program Analysis, Operational Semantics, Programming Languages, Program Transformation
    DOI
• 2014
  • With Shikar Kumar and Coty Gonzalez: How people do relational reasoning? Role of problem complexity and domain familiarity, Computers in Human Behavior — CHB, vol. 41, 319-326, Elsevier, December 2014. Relational reasoning; Problem solving; Spreadsheet; Domain familiarity; Problem complexity
    papers/chb14.pdfDOI
  • With Edmund S.L. Lam: Optimized Compilation of Multiset Rewriting with Comprehensions, 12th Asian Symposium on Programming Languages and Systems — APLAS'14 (Jacque Garrigue, editor), 19-38, Springer LNCS 8858, Singapore, 17 November 2014. Springer. Multiset Rewriting, Forward Logic Programming, Comprehension, Compilation, Join Ordering
    papers/aplas14.pdfDOIby Edmund S.L. Lam
  • With Yuxin Deng and Robert J. Simmons: Relating reasoning methodologies in linear logic and process algebra, Mathematical Structures in Computer Science — MSCS, 1-39, Cambridge University Press, December 2014. Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition system
    papers/mscs14.pdfDOIFirstView
  • With Jorge Luis Sacchini, Frank Pfenning and Carsten Schürmann: Mode checking in the Concurrent Logical Framework, Technical Report CMU-CS-14-134, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 2014. Mode Checking, Logical Frameworks, Concurrent Logical Framework
    papers/cmu-cs-14-134.pdf
  • With Edmund S.L. Lam: Constraint Handling Rules with Multiset Comprehension Patterns, 11th International Workshop on Constraint Handling Rules — CHR'14 (Rémy Haemmerlé and Jon Sneyers, editors), Vienna, Austria, 18 July 2014. Programming languages; multiset; rewriting; CHR; comprehension.
    papers/chr14.pdfarXiv
  • With Edmund S.L. Lam: Reasoning About Set Comprehensions, 12th International Workshop on Satisfiability Modulo Theories — SMT'14, CEUR Workshop Proceedings, vol. 1163 (Philipp Rümmer and Christoph Wintersteiger, editors), 27-37, Vienna, Austria, 17-18 July 2014. Programming languages; multiset; rewriting; CHR; comprehension; SMT solver; set
    papers/smt14.pdfby Edmund S.L. Lam
  • Proof-Theoretic Foundations of Indexing in Logic Programming, 9th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice — LFMTP'14 (Amy Felty and Brigitte Pientka, editors), Vienna, Austria, 17 July 2014. Programming languages; logic programming; proof-theory; foundations; indexing; linear; focusing.
    papers/lfmtp14.pdfDOI
  • With Edmund S.L. Lam: Optimized Compilation of Multiset Rewriting with Comprehensions, Technical Report CMU-CS-14-119, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, June 2014. Multiset Rewriting, Logic Programming, Comprehension, Compilation, Join Ordering
    papers/cmu-cs-14-119.pdf
  • With Thierry Sans: Substructural Meta-Theory of a Type-Safe Language for Web Programming, Fundamenta Informaticae, vol. 130(1), 1-31, IOS Press, 2014. web programming; type safety; substructural operational semantics; SSOS; parallelism; mobile code; substructural meta-theory
    papers/fi14.pdf
• 2013
  • With Thierry Sans and Soha Hussein: Controlling Data Flow with a Policy-Based Programming Language for the Web, 18th Nordic Conference on Secure IT Systems — NordSec'13 (Dieter Gollmann and Hanne Riis Nielson, editors), 215-230, Springer-Verlag LNCS 8208, Ilulissat, Greenland, 18-21 October 2013. Springer-Verlag. Distributed data flow; type-safety; security policies
    papers/nordsec13.pdf
  • With Edmund S.L. Lam: Decentralized Execution of Constraint Handling Rules for Ensembles, 15th International ACM Symposium on Principles and Practice of Declarative Programming — PPDP'13 (Tom Schrijvers, editor), 205-216, Madrid, Spain, 16-18 September 2013. ACM. Distributed Programming, Constraint Logic Programming, Multiset Rewriting
    papers/ppdp13.pdfby Edmund S.L. Lam
  • The Deductive Spreadsheet (ISBN: 978-3-642-37746-4) , Springer-Verlag, September 2013. Cognitive interface design, Deductive decision-making, End-users, Explanation support, Fixpoints, Graphical user interface, Logic programming, Relational algebra, Spreadsheet paradigm, Usability analysis
    Springeramazon.comcover
  • With Jorge Luis Sacchini: Towards Meta-Reasoning in the Concurrent Logical Framework CLF, Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics — EXPRESS/SOS'13 (Johannes Borgström and Bas Luttik, editors), Buenos Aires, Argentina, 26 August 2013. Meta-reasoning; CLF; logical framework; meta-logical framework
    papers/express13.pdfby Jorge Luis Sacchini
  • With Edmund S.L. Lam: Decentralized Execution of Constraint Handling Rules for Ensembles, Technical Report CMU-CS-13-106, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, April 2013. Distributed Programming, Constraint Logic Programming, Multiset Rewriting
    papers/cmu-cs-13-106.pdf
• 2012
  • With Yuxin Deng and Robert J. Simmons: Relating Reasoning Methodologies in Linear Logic and Process Algebra, Electronic Proceedings in Theoretical Computer Science — ETPCS, vol. 101, 50-60, November 2012. Extended version of LINEARITY'12.Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition system
    papers/eptcs12.pdfArXivInfo
  • With Edmund S.L. Lam: Modeling Datalog Fact Assertion and Retraction in Linear Logic, 14th International ACM Symposium on Principles and Practice of Declarative Programming — PPDP'12 (Andy King, editor), 67-78, Leuven, Belgium, 19-21 September 2012. ACM. Datalog, assertion, remotion, truth management, linear logic, correctness
    papers/ppdp12.pdfby Edmund S.L. Lam
  • With Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Robert J. Simmons: Trace Matching in a Concurrent Logical Framework, 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice — LFMTP'12 (Adam Chlipala and Carsten Schürmann, editors), Copenhagen, Denmark, 9 September 2012. ACM. CLF, Concurrent traces, epsilon, matching
    papers/lfmtp12.pdfby Jorge Luis Sacchini
  • An Improved Proof-Theoretic Compilation of Logic Programs, Theory and Practice of Logic Programming — TPLP, vol. 12(4-5) (Agostino Dovier and Vítor Santos Costa, editors), 639-657, Cambridge University Press, 2012. Special Issue on the 28th International Conference on Logic Programming — ICLP'12, Budapest, Hungary, 4-8 September 2012.Compilation; Abstract Logic Programming; Hereditary Harrop Formulas; Well-Moded Logic Programs
    papers/iclp12.pdfICLP'12arXivvideo
  • With Edmund S.L. Lam: Modeling Datalog Fact Assertion and Retraction in Linear Logic, Technical Report CMU-CS-12-126, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 2012. Datalog, Linear Logic, Retraction, Assertion, Dynamic updates
    papers/cmu-cs-12-126.pdf
  • With Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Robert J. Simmons: On Matching in CLF, Technical Report CMU-CS-12-114, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2012. CLF, concurrent traces, matching, unification, reasoning about concurrency
    papers/cmu-cs-12-114.pdf
  • With Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Robert J. Simmons: On Matching Concurrent Traces, 26th International Workshop on Unification — UNIF'12 (Santiago Escobar, Konstantin Korovin and Vladimir Rybakov, editors), Manchester, UK, 1 July 2012. Matching, parallel computation, computational traces
    papers/unif12.pdfby Jorge Luis Sacchini
  • With Yuxin Deng and Robert J. Simmons: Relating Reasoning Methodologies in Linear Logic and Process Algebra, Second International Workshop on Linearity — LINEARITY'12 (Sandra Alves and Ian Mackie, editors), Tallinn, Estonia, 1 April 2012. Linear logic, process algebra, induction, coinduction, contextual preorder, simulation, labeled transition system
    papers/linearity12.pdf
• 2011
  • With Yuxin Deng and Robert J. Simmons: Relating Reasoning Methodologies in Linear Logic and Process Algebra, Technical Report CMU-CS-11-145, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, December 2011. Linear logic, process algebra, CCS, pi-calculus, meta-reasoning, logical preorder, contextual preorder, simulation, labeled transition systems, equivalence, induction, coinduction
    papers/cmu-cs-11-145.pdf
  • MSR 2.0: Language Definition and Programming Environment, Technical Report CMU-CS-11-141, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, November 2011. MSR 2.0, multiset rewriting, specification language, language definition, syntax, typing, execution, type reconstruction, CMUQ, NPRP 09-667-1-100
    papers/cmu-cs-11-141.pdf
  • Typed Multiset Rewriting Specifications of Security Protocols, Technical Report CMU-CS-11-140, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, October 2011. Specification of Security Protocol, Dolev-Yao Model, Parallel Multiset Rewriting, Dependent Types, Subsorting, Data Access Specification, Dolev-Yao Intruder, Strongest Attacker, CMUQ, NPRP 09-667-1-100
    papers/cmu-cs-11-140.pdf
  • With Andreas Karatsolis, Nael Abu-Ghazaleh, Yonina Cooper, Khaled Harras, Kemal Oflazer and Thierry Sans: Getting CS Undergraduates to Communicate Effectively, 16th Annual AMC Conference on Innovation and Technology in Computer Science Education — ITiCSE'11 (Guido Rößling, Tom Naps and Christian Spannagel, editors), 283-287, ACM Press, Darmstadt, Germany, 27-29 June 2011. ACM. Computer Science Education, CS Education, Writing
    papers/iticse11.pdf
  • Discovering Logic through Comics, 16th Annual AMC Conference on Innovation and Technology in Computer Science Education — ITiCSE'11 (Guido Rößling, Tom Naps and Christian Spannagel, editors), 103-107, ACM Press, Darmstadt, Germany, 27-29 June 2011. ACM. Computer Science eduction, freshmen year, first-year of college, logic, computational thinking, comic book, logicomix, communication skills, history of CS
    papers/iticse11a.pdf
  • With Andreas Karatsolis, Nael Abu-Ghazaleh, Yonina Cooper, Khaled Harras, Kemal Oflazer and Thierry Sans: A Framework to Support the Communication Needs of CS Undergraduates (short paper) , 42nd ACM Technical Symposium on Computer Science Education — SIGCSE'11 (Thomas Cortina, Ellen Walker and Laurie Smith King, editors), 711, ACM Press, Dallas, TX, 9-12 March 2011. ACM. Computer Science Education, CS Education, Writing
    papers/sigcse11.pdf
  • With Michael Backes, Aaron D. Jaggard, Andre Scedrov and Joe-Kai Tsay: Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos, International Journal of Information Security — IJIS, vol. 10(2), 107-134, Springer Verlag, 2011. Security, Kerberos, Dolev-Yao model, PKINIT, computational model
    papers/ijis11.pdfweb
• 2010
  • With Thierry Sans: QWeSST for Type-Safe Web Programming, Third International Workshop on Logics, Agents, and Mobility — LAM'10, EPiC, vol. 7(1) (Berndt Farwer, editor), 96-111, EasyChair Publications, Edinburgh, Scotland, UK, 15 July 2010. Web programming, type safety, Qwesst, mobile
    papers/lam10.pdfweb
  • With Thierry Sans: Type-Safe Web Programming in QWeSST, Technical Report CMU-CS-10-125, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, June 2010. Web programming, type safety, Qwesst, mobile, parallelism
    papers/cmu-cs-10-125.pdf
• 2009
  • With Andre Scedrov: Relating State-Based and Process-Based Concurrency through Linear Logic, Information & Computation, vol. 207(10), 1044-1077, Elsevier, October 2009. Elsevier. linear logic, Petri nets, multiset rewriting, process algebra, security
    papers/ic09.pdfweb
• 2008
  • With Helmut Veith and Andrei Voronkov (co-editors): Logic for Programming, Artificial Intelligence and Reasoning (ISBN: 978-3-540-89438-4) , Proceedings of the 15th International conference — LPAR'08, Springer-Verlag LNCS 5330, 713 + XI, Doha, Qatar, November 2008. Springer-Verlag.
  • On Teaching Programming Languages Using a Wiki, The 2008 Communication Symposium at Carnegie Mellon University: Developing Disciplinary Literacy — CS'08 (D. Wetzel, editor), 1-3, Pittsburgh, PA, 9-11 June 2008.
    papers/cs08.pdf
  • With Aaron D. Jaggard, Joe-Kai Tsay, Andre Scedrov and Christopher Walstad: Breaking and Fixing Public-Key Kerberos, Information & Computation, vol. 206(2-4), 402-424, Elsevier, April 2008. Elsevier. Security, Kerberos, Dolev-Yao model, PKINIT
    papers/ic07.pdf
• 2007
  • Advances in Computer Science: Computer and Network Security, Proceedings of the 12th Annual Asian Computing Conference — ASIAN'07, Springer-Verlag LNCS 4846, 310 + XI, Doha, Qatar, December 2007. Springer-Verlag.
  • NEXCEL, a Deductive Spreadsheet, The Knowledge Engineering Review, vol. 22, 221-236, November 2007.
    papers/ker06.pdf
  • With Kevin Watkins, Frank Pfenning and David Walker: Specifying Properties of Concurrent Computations in CLF, Fourth Workshop on Logical Frameworks and Meta-languages — LFM'04 (Carsten Schuermann, editor), 67-87, Elsevier ENTCS 199, Cork, Ireland, 5 July 2004, revised October 2007. Elsevier.
    papers/lfm04.pdfweb
  • With Catherine Meadows: One Picture is Worth a Dozen Connectives: A Fault-Tree Representation of NPATRL Security Requirements, IEEE Transactions on Dependable and Secure Computing, vol. 4(3), 216-227, IEEE Computer Society Press, July 2007.
    papers/tdsc07.pdfweb
  • With Mark-Oliver Stehr: Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types, Higher-Order and Symbolic Computation, vol. 20(1/2) (Narciso Martí-Oliet, Grigore Rosu and Carolyn Talcott, editors), 3-35, Kluwer Academic Publishing, June 2007.
    papers/hocs07.pdfweb
• 2006
  • With Aaron D. Jaggard, Joe-Kai Tsay, Andre Scedrov and Christopher Walstad: Breaking and Fixing Public-Key Kerberos, Eleventh Annual Asian Computing Science Conference — ASIAN'06 (Mitsu Okada and Ichiro Satoh, editors), 167-181, Springer-Verlag LNCS 4435, Tokyo, Japan, 6-8 December 2006. Springer-Verlag. Post-conference proceedings.
    papers/asian06.pdfweb
  • With Catherine Meadows and Dusko Pavlovic: Deriving Key Distribution Protocols and their Security Properties, Technical Report CMU-CS-06-172, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, June 2005, revised December 2006.
    papers/cmu-cs-06-172.pdf
  • With Frederic Butler, Aaron D. Jaggard, Andre Scedrov and Christopher Walstad: Formal Analysis of Kerberos 5, Theoretical Computer Science, vol. 367(1-2), 57-87, November 2006.
    papers/tcs06.pdfweb
  • A Spreadsheet for Everyday Symbolic Reasoning, AAAI 2006 Fall Symposium on Integrating Reasoning into Everyday Applications — EVERYDAY'06 (M. Kassoff, H. Stuckenschmidt, A. Valente and M. Witbrock, editors), 1-8, Technical Report FS-06-04 (AAAI Press), Arlington, VA, 14 October 2006.
    papers/aaai06f.pdf
  • With Michael Backes, Aaron D. Jaggard, Andre Scedrov and Joe-Kai Tsay: Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos, 11th European Symposium On Research In Computer Security — ESORICS'06 (D. Gollmann and A. Sabelfeld, editors), 362-383, IEEE Computer Society Press, Hamburg, Germany, 18-20 September 2006.
    papers/esorics06.pdfwebby Joe-Kai Tsay
  • With Andre Scedrov: Relating State-Based and Process-Based Concurrency through Linear Logic, 13th Workshop on Logic, Language, Information and Computation — WoLLIC'06 (Ruy de Queiroz, editor), 145-176, Elsevier ENTCS 165, Stanford, CA, 18-21 July 2006.
    papers/wollic06.pdfweb
  • With Aaron D. Jaggard, Joe-Kai Tsay, Andre Scedrov and Christopher Walstad: Breaking and Fixing Public-Key Kerberos, Sixth Workshop on Issues in the Theory of Security — WITS'06 (Dieter Gollmann and Jan Jürjens, editors), 55-70, Vienna, Austria, 25-26 March 2006.
    papers/wits06.pdf
  • Towards a Notion of Quantitative Security Analysis, Quality of Protection: Security Measurements and Metrics — QoP'05 (Dieter Gollmann, Fabio Massacci and Artsiom Yautsiukhin, editors), 131-144, Springer-Verlag Advances in Information Security 23, 2006. Springer-Verlag. Revised Papers of the First Workshop on Quality of Protection, Milan, Italy, 15 September 2005.
    papers/qop05.pdf
• 2005
  • The Deductive Spreadsheet, Technical Report DS05-02, Deductive Solutions, Annandale, VA, August 2005.
  • With Catherine Meadows and Dusko Pavlovic: An Encapsulated Authentication Logic for Reasoning About Key Distribution Protocol, Eighteenth Computer Security Foundations Workshop — CSFW-18, 48-61, IEEE Computer Society Press, Aix-en-Provence, France, 20-22 June 2005.
    papers/csfw05.pdf
  • With Nancy Durgin, Patrick D. Lincoln, John C. Mitchell and Andre Scedrov: A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis, Journal of Computer Security, vol. 13(2), 265-316, IOS Press, April 2005.
    papers/jcs05b.pdfweb
  • The Deductive Spreadsheet: Mid-Project Report, Technical Report DS05-01, Deductive Solutions, Annandale, VA, March 2005.
  • With Stefano Bistarelli, Gabriele Lenzini and Fabio Martinelli: Relating Multiset Rewriting and Process Algebras for Security Protocol Analysis, Journal of Computer Security, vol. 13(1) (Roberto Gorrieri, editor), 3-47, IOS Press, February 2005.
    papers/jcs05a.pdfweb
  • With Serge Autexier and Heiko Mantel: Special issue on FCS/VERIFY 2002, International Journal of Information Security, vol. 4(1), February 2005.
  • With Aaron D. Jaggard, Andre Scedrov and Christopher Walstad: Specifying Kerberos 5 Cross-Realm Authentication, Fifth Workshop on Issues in the Theory of Security — WITS'05 (Catherine Meadows and Jan Jürjens, editors), 12-26, ACM Digital Library, Long Beach, CA, 10-11 January 2005.
    papers/wits05.pdfwebby Christopher Walstad
• 2004
  • With Catherine Meadows and Paul F. Syverson: Formal Specification and Analysis of the Group Domain of Interpretation using NPATR and the NRL Protocol Analyzer, Journal of Computer Security, vol. 12(6) (Sabrina De Capitani di Vimercati, editor), 893-932, IOS Press, November 2004.
    papers/jcs04.pdfweb
  • The Logical Meeting Point of Multiset Rewriting and Process Algebra: Progress Report, Technical Memo CHACS-5540-153, Center for High Assurance Computer Systems, Naval Research Laboratory, Washington, DC, September 2004.
    papers/chacs-5540-153.pdf
  • Fine-Grained MSR Specifications for Quantitative Security Analysis, Fourth Workshop on Issues in the Theory of Security — WITS'04 (Peter Ryan, editor), 111-127, Barcelona, Spain, 3-4 April 2004.
    papers/wits04.pdf
  • With Frederic Butler, Aaron D. Jaggard and Andre Scedrov: A Formal Analysis of Some Properties of Kerberos 5 Using MSR, Technical Report MS-CIS-04-04, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, April 2004.
    papers/ms-cis-04-04.pdf
  • With Mark-Oliver Stehr: 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 (Narciso Martí-Oliet, editor), 183-207, Elsevier ENTCS 117, Barcelona, Spain, 27-28 March 2004.
    papers/wrla04.pdfweb
• 2003
  • With Frank Pfenning: A Linear Spine Calculus, Journal of Logic and Computation, vol. 13(5), 639-688, Oxford University Press, December 2003.
    papers/jlc03.pdf
  • With Frederic Butler, Aaron D. Jaggard and Andre Scedrov: Verifying Confidentiality and Authentication in Kerberos 5 in Software Security: Theories and Systems — ISSS 2003 (K. Futatsugi, F. Mizoguchi and N. Yonezaki, editors), 1-24, Springer-Verlag LNCS 3233, Tokyo, Japan, 4-6 November 2003. Springer-Verlag. Revised Papers of the 2003 Mext-NSF-JSPS International Symposium.
    papers/isss03.pdf
  • With Stefano Bistarelli, Gabriele Lenzini and Fabio Martinelli: Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols, Second International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security — MMM'03 (V.I. Gorodetski, V.A. Skormin and L.J. Popyack, editors), 86-99, Springer-Verlag LNAI 2776, St. Petersburg, Russia, 20-24 September 2003. Springer-Verlag.
    papers/mmm03.pdf
  • Foundations of Computer Security, proceedings of the LICS'03 workshop — FCS'03, Technical Report TR-2003-04, Department of Computer Science, University of Ottawa, Ottawa, Canada, 26-27 June 2003.
    papers/fcs03.pdfcoverbibtex of papers
  • With Kevin Watkins, Frank Pfenning and David Walker: A Concurrent Logical Framework I: Judgments and Properties, Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, March 2002, revised May 2003.
    papers/cmu-cs-02-101.pdf
  • With Frank Pfenning, David Walker and Kevin Watkins: A Concurrent Logical Framework II: Examples and Applications, Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, March 2002, revised May 2003.
    papers/cmu-cs-02-102.pdf
  • With Frank Pfenning, Kevin Watkins and David Walker: A Concurrent Logical Framework: The Propositional Fragment, TYPES Conference — TYPES'03 (Stefano Berardi, Mario Coppo and Ferruccio Damiani, editors), 355-377, Springer-Verlag LNCS 3085, Torino, Italy, 30 April - 4 May 2003. Springer-Verlag. Post-conference proceedings.
    papers/types03.pdf
  • With Catherine Meadows: A Fault-Tree Representation of NPATRL Security Requirements, Third Workshop on Issues in the Theory of Security — WITS'03 (R. Gorrieri, editor), 1-10, Warsaw, Poland, 5-6 April 2003.
    papers/wits03a.pdf
  • With Stefano Bistarelli, Gabriele Lenzini and Fabio Martinelli: Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis, Third Workshop on Issues in the Theory of Security — WITS'03 (R. Gorrieri, editor), 21-31, Warsaw, Poland, 5-6 April 2003.
    papers/wits03b.pdf
  • With Fabio Martinelli, Stefano Bistarelli, Gabriele Lenzini and Roberto Marangoni: Representing Biological Systems through Multiset Rewriting, Workshop on Computational Methods in Biomathematics — CMB'03, Las Palmas de Gran Canaria, Spain, 26 February 2003.
    papers/cmb03.pdf
  • With Stefano Bistarelli, Gabriele Lenzini, Roberto Marangoni and Fabio Martinelli: On Representing Biological Systems through Multiset Rewriting, Nineth International Workshop on Computer Aided System Theory — EUROCAST'03 (Roberto Moreno-Díaz and Franz Pichler, editors), 415-426, Springer-Verlag LNCS 2809, Las Palmas de Gran Canaria, Spain, 24-28 February 2003. Springer-Verlag.
    papers/eurocast03.pdf
• 2002
  • Data Access Specification and the Most Powerful Symbolic Attacker in MSR in Software Security: Theories and Systems — ISSS 2002 (M. Okada, B. Pierce, Andre Scedrov, H. Tokuda and A. Yonezawa, editors), 384-416, Springer-Verlag LNCS 2609, Tokyo, Japan, 8-10 November 2002. Springer-Verlag. Revised Papers of the 2002 Mext-NSF-JSPS International Symposium.
    papers/isss02a.pdf
  • With Nancy Durgin, Patrick D. Lincoln, John C. Mitchell and Andre Scedrov: A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis in Software Security: Theories and Systems — ISSS 2002 (M. Okada, B. Pierce, Andre Scedrov, H. Tokuda and A. Yonezawa, editors), 356-383, Springer-Verlag LNCS 2609, Tokyo, Japan, 8-10 November 2002. Springer-Verlag. Revised Papers of the 2002 Mext-NSF-JSPS International Symposium.
    papers/isss02b.pdf
  • With Frank Pfenning: A Linear Logical Framework, Information & Computation, vol. 179(1), 19-75, November 2002.
    papers/ic02.pdf
  • Foundations of Computer Security, proceedings of the FLoC'02 Workshop on Foundations of Computer Security — FCS'02, Technical Report DIKU-02-12, Department of Computer Science, University of Copenhagen, Copenhagen, Denmark, 25-26 July 2002.
    papers/fcs02.pdfpdfbibtex of papers
  • Solution Count for Multiset Unification with Trailing Multiset Variables, Sixteenth International Workshop on Unification — UNIF'02 (C. Ringeissen, C. Tinelli, F. Trinen and R. Verma, editors), 64-68, Technical Report 02-05 (Department of Computer Science, University of Iowa), Copenhagen, Denmark, 25-26 July 2002.
    papers/unif02.pdf
  • With Frederic Butler, Aaron D. Jaggard and Andre Scedrov: A Formal Analysis of Some Properties of Kerberos 5 Using MSR, Fifteenth Computer Security Foundations Workshop — CSFW-15, 175-190, IEEE Computer Society Press, Cape Breton, NS, Canada, 24-26 June 2002.
    papers/csfw02.pdf
  • With Jonathan Herzog (co-editor): The Computer Security Foundations Workshop: 1988-2002, CD-ROM, June 2002.
  • The Wolf Within, Second Workshop on Issues in the Theory of Security — WITS'02 (J. Guttman, editor), Portland, OR, 14-15 January 2002.
    papers/wits02.pdf
• 2001
  • A Specification Language for Crypto-Protocols based on Multiset Rewriting, Dependent Types and Subsorting, Workshop on Specification, Analysis and Validation for Emerging Technologies — SAVE'01 (G. Delzanno, S. Etalle and M. Gabbrielli, editors), 1-22, Paphos, Cyprus, 1 December 2001.
    papers/save01.pdf
  • With Catherine Meadows and Paul F. Syverson: Formalizing GDOI Group Key Management Requirements in NPATRL, 8th ACM Conference on Computer and Communication Security — CCS'01 (P. Samarati, editor), 235-244, ACM Press, Philadelphia, PA, 6-8 November 2001. ACM.
    papers/
  • The Dolev-Yao Intruder is the Most Powerful Attacker, 16th Annual Symposium on Logic in Computer Science — LICS'01 (J. Halpern, editor), IEEE Computer Society Press, Boston, MA, 16-19 June 2001.
    papers/lics01.pdf
  • Typed MSR: Syntax and Examples, First International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security — MMM'01 (V.I. Gorodetski, V.A. Skormin and L.J. Popyack, editors), 159-177, Springer-Verlag LNCS 2052, St. Petersburg, Russia, 21-23 May 2001. Springer-Verlag.
    papers/mmm01.pdfphotos
  • With Paul F. Syverson: The Logic of Authentication Protocols in Foundations of Security Analysis and Design (R. Focardi and R. Gorrieri, editors), 63-136, Springer-Verlag LNCS 2171, 2001.
    papers/fosad00.pdf
• 2000
  • With Nancy Durgin, Max I. Kanovich and Andre Scedrov: Interpreting Strands in Linear Logic, 2000 Workshop on Formal Methods and Computer Security — FMCS'00 (H. Veith, N. Heintze and E. Clark, editors), Chicago, IL, 20 July 2000.
    papers/fmcs00.pdf
  • Typed Multiset Rewriting Specifications of Security Protocols, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology — MFCSIT'00 (A. Seda, editor), 1-43, Elsevier ENTCS 40, Cork, Ireland, 19-21 July 2000.
    papers/entcs01.pdfweb
  • With Catherine Meadows and Paul F. Syverson: Dolev-Yao is no better than Machiavelli, First Workshop on Issues in the Theory of Security — WITS'00 (P. Degano, editor), Geneva, Switzerland, 8-9 July 2000.
    papers/wits00.pdf
  • With Angelo Montanari: A Calculus of Macro-Events: Progress Report, 7th International Workshop on Temporal Representation and Reasoning — TIME'00 (A. Trudel and S.D. Goodwin, editors), 47-58, IEEE Computer Society Press, Cape Breton, Nova Scotia, Canada, 7-9 July 2000.
    papers/time00.pdf
  • With Nancy Durgin, Patrick D. Lincoln, John C. Mitchell and Andre Scedrov: Relating Strands and Multiset Rewriting for Security Protocol Analysis, 13th Computer Security Foundations Workshop — CSFW-13, 35-51, IEEE Computer Society Press, Cambridge, UK, 3-5 July 2000.
    papers/csfw00.pdfweb
  • With Massimo Franceschet and Angelo Montanari: A Guided Tour through some Extensions of the Event Calculus, Computational Intelligence, vol. 16(2), 307-347, May 2000.
    papers/ci00.pdf
  • With Joshua S. Hodas and Frank Pfenning: Efficient Resource Management for Linear Logic Proof Search, Theoretical Computer Science, vol. 232(1-2), 133-163, February 2000.
    papers/tcs00.pdf
  • Logical Framework Design: Why not just classical logic? in Formalizing the Dynamics of Information (M. Faller, S. Kaufmann and M. Pauly, editors), 87-104, CSLI Publications, 2000.
    papers/csli00.pdf
• 1999
  • With Valeria de Paiva and Eike Ritter: Explicit Substitutions for Linear Logical Frameworks: Preliminary Results, Workshop on Logical Frameworks and Meta-languages — LFM'99 (A. Felty, editor), Paris, France, 28 September 1999.
    papers/lfm99.pdf
  • With John C. Mitchell (co-editor): Pleiades Project: Collected Work 1998-1999, Technical Report STAN-CS-TR-99-1625, Department of Computer Science, Stanford University, Stanford, CA, August 1999.
    papers/muri99.pdf
  • With Nancy Durgin, Patrick D. Lincoln, John C. Mitchell and Andre Scedrov: A Meta-Notation for Protocol Analysis, 12th Computer Security Foundations Workshop — CSFW-12, 55-69, IEEE Computer Society Press, Mordano, Italy, 28-30 June 1999.
    papers/csfw99.pdfweb
  • With Angelo Montanari: A General Modal Framework for the Event Calculus and its Skeptical and Credulous Variants, Journal of Logic Programming, vol. 38(2), 111-164, February 1999.
    papers/jlp99.pdf
• 1998
  • With John C. Mitchell (co-editor): Pleiades Project: Collected Work 1997-1998, Technical Report STAN-CS-TR-98-1612, Department of Computer Science, Stanford University, Stanford, CA, September 1998.
    papers/muri98.pdf
  • Proof-Theoretic Foundation of Compilation in Logic Programming Languages, 1998 Joint International Conference and Symposium on Logic Programming — JICSLP'98 (J. Jaffar, editor), 115-129, MIT Press, Manchester, UK, 16-19 June 1998.
    papers/jicslp98.pdf
  • With Massimo Franceschet and Angelo Montanari: The Complexity of Model Checking in Modal Event Calculi with Quantifiers, 6th International conference on Principles of Knowledge Representation and Reasoning — KR'98 (A.G. Cohn, L.K. Shubert and S.C. Shapiro, editors), 368-379, Morgan Kaufmann publishers, Trento, Italy, 2-5 June 1998.
    papers/kr98.pdf
  • With Massimo Franceschet and Angelo Montanari: Event Calculus with Explicit Quantifiers, 5th International Workshop on Temporal Representation and Reasoning — TIME'98 (R. Morris and L. Khatib, editors), 81-88, IEEE Computer Society Press, Sanibel Island, FL, 16-17 May 1998.
    papers/time98.pdf
  • With Massimo Franceschet and Angelo Montanari: The Complexity of Model Checking in Modal Event Calculi with Quantifiers, Electronic Transactions in Artificial Intelligence, vol. 2(1-2), 1-24, January-June 1998.
    papers/etai98.pdfwebweb
• 1997
  • With Massimo Franceschet and Angelo Montanari: A Hierarchy of Modal Event Calculi: Expressiveness and Complexity, 2nd International Conference on Temporal Logic — ICTL'97 (H. Barringer, M. Fisher, M. Gabbay and G. Gough, editors), 1-17, Manchester, UK, 14-18 July 1997.
    papers/ictl97.pdfweb
  • With Massimo Franceschet and Angelo Montanari: The Complexity of Model Checking in Modal Event Calculi, 14th International Conference on Logic Programming — ICLP'97 (L. Naish, editor), 419, MIT Press, Leuven, Belgium, 8-12 July 1997.
    papers/iclp97.pdf
  • With Frank Pfenning: Linear Higher-Order Pre-Unification, Technical Report CMU-CS-97-160, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 1997.
    papers/cmu-cs-97-160.pdfweb
  • With Frank Pfenning: Linear Higher-Order Pre-Unification, 12th Annual Symposium on Logic in Computer Science — LICS'97 (G. Winskel, editor), 422-433, IEEE Computer Society Press, Warsaw, Poland, 29 June - 2 July 1997.
    papers/lics97.pdfweb
  • With Massimo Franceschet and Angelo Montanari: Modal Event Calculi with Preconditions, 4th International Workshop on Temporal Representation and Reasoning — TIME'97 (R. Morris and L. Khatib, editors), 38-45, IEEE Computer Society Press, Daytona Beach, FL, May 10-11 1997.
    papers/time97.pdf
  • With Frank Pfenning: A Linear Spine Calculus, Technical Report CMU-CS-97-125, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, April 1997.
    papers/cmu-cs-97-125.pdf
• 1996
  • With Luca Chittaro and Angelo Montanari: A General Modal Framework for the Event Calculus and its Skeptical and Credulous Variants, 12th European Conference on Artificial Intelligence — ECAI'96 (W. Wahlster, M. Fisher, M. Gabbay and G. Gough, editors), 33-37, John Wiley & Sons, Budapest, Hungary, 12-16 August 1996.
    papers/ecai96.pdf
  • With Frank Pfenning: Linear Higher-Order Pre-Unification, International Workshop on Proof-Search in Type-Theoretic Languages — PSTT'96 (D. Galmiche, editor), 41-50, New Brunswick, NJ, 30 July 1996.
    papers/pstt96.pdf
  • With Frank Pfenning: A Linear Logical Framework, 11th Annual Symposium on Logic in Computer Science — LICS'96 (E. Clarke, editor), 264-275, IEEE Computer Society Press, New Brunswick, NJ, 27-30 July 1996. This work appeared as Preprint 1834 of the Department of Mathematics of Technical University of Darmstadt, Germany. This paper was awarded the 2016 LICS Test-of-Time Award.
    papers/lics96.pdfweb
  • With Luca Chittaro and Angelo Montanari: A General Modal Framework for the Event Calculus and its Skeptical and Credulous Variants, Research Report 37/96-RR, Dipartimento di Matematica e Informatica, Università di Udine, Udine, Italy, July 1996.
    papers/udmi-37_96.pdfweb
  • With Joshua S. Hodas and Frank Pfenning: Efficient Resource Management for Linear Logic Proof Search, International Workshop on Extensions of Logic Programming — ELP'96 (R. Dyckhoff, H. Herre and P. Schröder-Heister, editors), 67-81, Springer-Verlag LNAI 1050, Leipzig, Germany, 28-30 March 1996. Springer-Verlag.
    papers/elp96.pdf
  • Un Logical Framework Lineare (in Italian) Tesi di Dottorato di Ricerca in Informatica, Università degli Studi di Torino, Torino, Italy, February 1996. The English version will be shortly available.
    papers/thesis_to.pdf
• 1995
  • Petri Nets and Linear Logic: a case study for logic programming, 1995 Joint Conference on Declarative Programming — GULP-PRODE'95 (M. Apuente and M.I. Sessa, editors), 313-318, Palladio Press, Marina di Vietri, Italy, 11-14 September 1995.
    papers/gulp95.pdf
  • With Luca Chittaro and Angelo Montanari: A Modal Calculus of Partially Ordered Events in a Logic Programming Framework, 12th International Conference on Logic Programming — ICLP'95 (L. Sterling, editor), 299-313, MIT Press, Kanagawa, Japan, 13-16 June 1995.
    papers/iclp95.pdf
  • With Luca Chittaro and Angelo Montanari: Speeding up Temporal Reasoning by Exploiting the Notion of Kernel of an Ordering Relation, 2nd International Workshop on Temporal Representation and Reasoning — TIME'95 (S.D. Goodwin and H.J. Hamilton, editors), 73-80, Melbourne Beach, FL, 26 April 1995.
    papers/time95.pdfweb
• 1994
  • With Luca Chittaro and Angelo Montanari: Modal Event Calculus (short paper) , 1994 International Logic Programming Symposium — ILPS'94 (M. Bruynooghe, editor), 675, MIT Press, Ithaca, NY, 14-17 November 1994.
    papers/ilps94.pdf
  • With Luca Chittaro and Angelo Montanari: What the Event Calculus does and How to do it Efficiently, 1994 Joint Conference on Declarative Programming — GULP-PRODE'94 (M. Apuente, R. Barbuti and I. Ramos, editors), 336-35, Peñíscola, Spain, 19-22 September 1994.
    papers/gulp94.pdfweb
  • With Luca Chittaro and Angelo Montanari: Modal Event Calculus in Lolli, Technical Report CMU-CS-94-198, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, September 1994.
    papers/cmu-cs-94-198.pdfweb
  • Lollipops taste of Vanilla too, Workshop on Proof-theoretical Extensions of Logic Programming — ELP'94 (A. Momigliano and M. Ornaghi, editors), 60-66, Santa Margherita Ligure, Italy, 18 June 1994.
    papers/elp94.pdf
• 1993
  • With Gianfranco Rossi: A WAM Implementation for the Logic Meta Programming Language 'Log, 8th Italian Conference on Logic Programming — GULP'93 (D. Saccà, editor), 203-214, Mediterranean Press, Gizzeria Lido, Italy, 15-18 June 1993.
    papers/gulp93.pdf
  • With Christoph F. Eick: Expression and Enforcement of Dynamic Integrity Constraints, First Italian Conference on Advanced Database Systems — SEBD'93 (D. Saccà, editor), 203-214, Mediterranean Press, Gizzeria Lido, Italy, 14-16 June 1993.
    papers/sebd93.pdf
  • With Angelo Montanari and Alessandro Provetti: On the Non-Monotonic Behavior of the Event Calculus for Deriving Maximal Time Intervals (special issue: Proceedings of the International Conference on Numerical Analysis with Automatic Result Verification, Lafayette, LA, 25 February - 1 March 1993, R. B. Kearfott guest editor) , International Journal on Interval Computations, vol. 2, 83-119, May 1993.
    papers/jic93.pdfweb
• 1992
  • With Christoph F. Eick: Specification and Enforcement of Dynamic Integrity Constraints, International Conference on Information and Knowledge Management — CIKM'92 (Y. Yesha, editor), 193-200, Baltimore, MD, 8-11 November 1992.
    papers/cikm92.pdf
  • A WAM Implementation for the Meta-Logic Programming Language 'LogMastersThesis, Department of Computer Science, University of Houston, Houston, TX, 24 July 1992.
    papers/master.pdf
  • With Gianfranco Rossi: Logic Meta-Programming Facilities in 'Log, 3rd International Workshop on Meta-Programming in Logic Programming — META'92 (A. Pettorossi, editor), 148-161, Springer-Verlag LNCS 649, Uppsala, Sweden, 10-12 June 1992. Springer-Verlag.
    papers/meta92.pdfweb
• 1991
  • With Gianfranco Rossi: Logic Meta-Programming in 'Log, Research Report 14/91-RR, Dipartimento di Matematica e Informatica, Università di Udine, Udine, Italy, October 1991.
    papers/gulp91.shtml
  • With Gianfranco Rossi: Meta-Programmazione Logica in 'Log (in Italian) , 6th Italian Conference on Logic Programming — GULP'91 (P. Asirelli, editor), 275-289, Pisa, Italy, 12-14 June 1991.
    papers/gulp91.pdf
  • Una Proposta per l'Introduzione di Capacità di Meta-Rappresentazione in un Linguaggio di Programmazione Logica (in Italian) Tesi di Laurea in Scienze dell'Informazione, Università degli Studi di Udine, Udine, Italy, 7 March 1991.