Theorem proving, automated deduction,
Preuves sur ordinateur, démonstration automatique,
- CSI 4900 Projets de recherche/Honours Project, Fall 2012 and Winter 2013
- CSI 3104 Introduction to Formal Languages, Winter 2013
- CSI 3504 Introduction aux langages formels, Hiver 2013
- CSI 5110 Principles of Formal Software Development, Fall 2012
Other Recent Courses
- ITI 1120 Introduction to Computing I, Winter 2008
- SEG 2105 Introduction to Software Engineering, Winter 2010
- CSI 2120 Programming Paradigms, Winter 2011
- CSI 2520 Paradigmes de programmation, Hiver 2012
- CSI 4125 Theory of Programming Languages, Winter 2008
- Software Correctness and Safety Research Laboratory
- The Logic and Foundations of Computing Group
- Publication List
- Co-Founder, Devera Logic, Inc.
- Journal of Applied Logic: Area Editor for Tactical Theorem Proving and Proof Planning, Elsevier
- Member, Committe on Logic in North America, Association for Symbolic Logic (ASL)
- Trustee, International Conference on Automated Deduction (CADE)
- Member, NSERC (National Science and Engineering Research Council of Canada) Computer Science Evaluation Group
- Member, Steering Committee, International Conference on Interactive Theorem Proving (ITP)
- Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), Nancy, France, September 16-19, 2013, Program Committee Member.
- 20th Workshop on Logic, Language, Information and Computation (WoLLIC 2013), Darmstadt, Germany, August 20-23, 2013, Program Committee Member.
- 2013 International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22-26, 2013, Program Committee Member.
- 24th International Conference on Automated Deduction (CADE 24) and affiliated workshops, Lake Placid, NY, USA, June 9-14, 2013.
- 2nd International Conference on Certified Programs and Proofs (CPP 2012), Kyoto, Japan, December 13-15, 2012, Program Committee Member.
- CV in pdf format
- 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 Information Technology and Engineering (SITE)
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
Contactez: L'École d'ingénierie et de technologie de l'information /
Contact: School of Information Technology and Engineering
Copyright © Université d'Ottawa / University of Ottawa
Webmestre / Webmaster