Theorem proving, automated deduction,
Preuves sur ordinateur, démonstration automatique,
- CSI 4900 Projets de recherche/Honours Project, Fall 2018 and Winter 2019
Other Recent Courses
- CSI 5140 Software Foundations, Fall 2016
- CSI 5110 Principles of Formal Software Development, Fall 2016
- CSI 4125 Theory of Programming Languages, Winter 2008
- CSI 3104 Introduction to Formal Languages, Winter 2017
- CSI 3504 Introduction aux langages formels, Hiver 2017
- SEG 2105 Introduction to Software Engineering, Winter 2010
- CSI 2120 Programming Paradigms, Winter 2011
- CSI 2520 Paradigmes de programmation, Hiver 2012
- ITI 1120 Introduction to Computing I, Winter 2008
- Software Correctness and Safety Research Laboratory
- The Logic and Foundations of Computing Group
- Two-Level Hybrid in Coq
- Publication List
- Treasurer, ACM Special Interest Group on Logic and Computation (SIGLOG)
- Journal of Automated Reasoning: Member of Editorial Board
- Journal of Applied Logic: Area Editor for Tactical Theorem Proving and Proof Planning, Elsevier
- IfCoLog Journal of Logics and their Applictions: Member of Editorial Board
- PeerJ Computer Science: Academic Editor in Theory & Formal Methods and Programming Languages
- Co-Founder, Devera Logic, Inc.
- 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, California, USA, January 2018, Program Co-Chair. Affiliated with the 2018 SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), January 8-13, 2018.
- International Symposium on Principles and Practice of Declarative Programming (PPDP 2017), Namur, Belgium, October 9-11, 2017, Program Committee Member.
- International Conference on Interactive Theorem Proving (ITP 2017), Brasília, Brazil, September 26-29, 2017, Steering Committee Member and Program Committee Member.
- International Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017), Brasília, Brazil, September 23-24, 2017, Program Committee Member.
- International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2017), Oxford, UK, September 8, 2017, Steering Committee Member and Program Committee Member.
- International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS 2017), Montreal, Quebec, Canada, August 24-25, 2017, Program Committee Member.
- 26th International Conference on Automated Deduction (CADE-26), Gothenburg, Sweden, August 6-11, 2017. Program Committee Member.
- Women in Logic Workshop (WiL 2017), Reykjavik, Iceland, June 19, 2017, Program Committee Member. Affiliated with the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), June 20-23, 2017.
- 7th International MCETECH Conference on e-Technologies (MCETECH 2017), Ottawa, Canada, May 17-19, 2017, Author.
- CV in pdf format
- Special Issue of Selected Extended Papers of CADE 2015, Journal of Automated Reasoning, 58(3), March 2017
- Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Springer Lecture Notes in Computer Science, Volume 9195, 2015
- Proceedings of the Ninth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'14)
- Proceedings of the Third International Conference on Interactive Theorem Proving (ITP'12), Springer Lecture Notes in Computer Science, Volume 7406
- Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'09)
- Notes (lecture 1 and lecture 2) on proof-carrying code for the June 2002 Summer School on the Proofs-as-Programs
- Proceedings of the 1999 Workshop on Logical Frameworks and Meta-languages (LFM'99)
- Some of my Lambda Prolog code specifying and implementing theorem provers
- A tutorial on Lambda Prolog and its Application to Theorem Proving.
School of Electrical Engineering and Computer Science (EECS)
University of Ottawa
800 King Edward Ave.
Ottawa, Ontario, Canada, K1N 6N5
Tel: (613) 562-5800 x6694, Fax: (613) 562-5664
Office: 5-068 SITE