News and Upcoming Events

• I gave a talk on "How to give a talk" at the Logic Mentoring Workshop @ LICS'19 in Vancouver!
• I gave the keynote at POPL'19 on Mechanizing Metatheory -- The Next Chapter, January 2019 (Video)
• Test of Time Award @ PPDP'18: B. Pientka and J. Dunfield, Programming with proofs and explicit contexts, published at PPDP'08. For a retrospective, check out my talk at PPDP'18 (slides)!
• I am the general chair of POPL 2020.
• I am on the PC for ESOP'19
• I am on the PC for FSCD'19
• I am on the SC of POPL (2017 - 2020).
• I am on the SC of ESOP (European Symposium on Programming Languages)( 2017 - 2020).
• I am one of the organizers of Logic Mentoring Workshop at FLOC'18 where I am giving a talk on How to get the most out of a conference!
• I am an invited speaker at Women in Logic Workshop at FLOC'18!
• I am an invited speaker at CPP'18!
• I am on the PC for the Workshop "Off the beaten track" OBT 2018 which is co-located with POPL.
• I am on the PC chair of PPDP'17 (9. Oct - 14. Oct. 2017)
• I am one of the organizers of the PLMW workshop co-locating at ICFP'17.
• I am a speaker at the Programming Languages Mentoring Workshop (PLMW'17) at POPL'17.
• I have been awarded a Humboldt Fellowship! Starting September I will be spending the academic year (until August 2018) at the Ludwig-Maximilian University Munich, Germany.

Recent Publications

• Brigitte Pientka, Ulrich Schoepp. Semantical Analysis of Contextual Types, FoSSaCS 2020.
• Aliya Hameer, Brigitte Pientka. Teaching the Art of Functional Programming Using Automated Grading (Experience Report) accepted at ICFP'19
• Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rebecca Zucchini. A Type Theory for Defining Logics and Proofs accepted at LICS'19
• David Thibodeau, Alberto Momigliano, Brigitte Pientka. A Case-Study in Programming Coinductive Proofs: Howe's Method, accepted at MSCS in 2018.
• Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. Index-Stratified Types, International Conference on Formal Structures for Computation and Deduction (FSCD'18): 19:1-19:17, LiPICS 2018
• Andrew Cave and Brigitte Pientka. Mechanizing Proofs with Logical Relations --Kripke-style, Mathematical Structures in Computer Science, accepted and in print June 2018.
• Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella, and Beluga, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD'17); more details, in particular the code for each case study can be found in the online repository.
• Aina Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka. Lincx: A Linear Logical Framework with First-Class Contexts, 26th European Symposium on Programming (ESOP'17), 2017
• Francisco Ferreira, Brigitte Pientka. Programs Using Syntax with First-Class Binders, 26th European Symposium on Programming (ESOP'17), 2017
• Amy Felty, Alberto Momigliano, Brigitte Pientka. Benchmarks for Reasoning with Syntax Trees Containing Binders and Contexts of Assumptions accepted in Mathematical Structures in Computer Science (MSCS), 2017.
• David Thibodeau, Andrew Cave, Brigitte Pientka. Indexed Codata Types (submitted March 2016), International Conference on Functional Programming (ICFP'16)
• Rohan Jacob-Rao, Andrew Cave and Brigitte Pientka. Mechanizing Proofs about Mendler-Recursion, 11th Workshop Logical Frameworks and Meta-languages (LFMTP'16): Theory and Practice, 2016

For a list of all publications see Research.

Recent Drafts

• Brigitte Pientka and Ulrich Schoepp, Semantical Analysis of Contextual Types, Feb 2019
• Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rebecca Zuccini, Cocon: Computation in Contextual Type Theory, Extended Technical Report, Jan 2019
• Brigitte Pientka, Andreas Abel, Guillaume Allais, Aliya Hameer, Alberto Momigliano, Steven Schaefer, Kathrin Stark. POPLMark Reloaded: Mechanizing Logical Relations Proofs, Dec 2018.
• Andreas Abel and Brigitte Pientka. Extensions to Miller's Pattern Unification for Dependent Types and Records, submitted July 2017

Software release

Check our Git Hub Repository for Beluga and the companion to Types and Programming Languages (TAPL).

Professional Activities

Talks

• Mechanizing Metatheory -- The Next Chapter, ACM Symposium on Programming Languages (POPL'19), January 2019
• POPLMark Reloaded: Mechanizing Logical Relations Proofs, International Conference on Certified Proofs and Programs (CPP'18), January 2018
• Mechanizing Meta-Theory in Beluga, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), June 2015
• Computational Thinking: What's the sience in Computer Science". This is a general talk for students with little or no background in computer science. I have given for example at the Undergraduate Cognitive Science Day and at Dawson College as part of their "Women in Science" day.
• Programming logical relations proofs, Brigitte Pientka, Certification of high-level and low-level programs, Institut Henri Poincare, Paris, France (slides)
• Beluga-mu: Programming proofs in context, Brigitte Pientka, POP Seminar, Carnegie Mellon University, May 2014 (slides)
• Beluga-mu: Programming proofs in context, Brigitte Pientka, Invited talk at International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP'12). (slides)
• Beluga: programming with contextual data, contexts, and ... , Brigitte Pientka, Invited talk at Programming Languages for Mechanized Mathematics Systems (PLMMS'10), July 2010, Paris, France
• Beluga: programming with dependent types, contextual data, and contexts, Brigitte Pientka, Invited talk at 10th International Symposium on Functional and Logic Programming (FLOPS'10), April 2010, Sendai, Japan.

Program Chair

• 19th Symposium on Principles and Practice of Declarative Programming (PPDP'17), 9. Oct. - 14. Oct. 2017, Namur, Belgium
• Formal Structures for Computation and Deduction (FSCD'16), 22. June - 26. June 2016, Port, Portugal.

Conference Chair

• 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'20)
• 22nd International Conference on Automated Deduction (CADE'09)

Editor

• Editorial Board of Journal of Functional Programming
• Editorial Board of ACM Transactions of Computational Logic (TOCL)
• Guest Editor for a special issue in Logical Methods in Computer Science for the best papers of FSCD'16 (Co-editor with Delia Kesner)
• Guest Editor for a special issue in Journal of Automated Reasoning for the best papers of CADE-22 (Co-editor with Renate Schmidt)
• Guest Editor for a special issue in Information and Computation on Intuitionistic Modal Logics and Applications (IMLA) (Co-editor with Valeria de Paiva)

Recent Program Committee

• 33rd ACM/IEEE Symposium on Logic in Computer Science LICS'18 which will be part of FLOC.
• Women in Logic (WIL) workshop (co-located with LICS'17)
• 32nd ACM/IEEE Symposium on Logic in Computer Science (LICS'17).
• 42nd ACM Symposium on Principles of Programming Languages (POPL 2016), Extended Review Committee
• Workshop on Type Directed Programming (TyDe), co-located with ICFP'16
• 25rd International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015
• 41st ACM Symposium on Principles of Programming Languages (POPL 2015)
• Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), Vienna, Austria, July 2014
• International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'14), July 2014, Vienna, Austria, as part of FLOC co-located with LICS'14 and IJCAR'14
• International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'13), Sept 2013, Boston, USA, co-located with ICFP'13.
• ACM Sigplan Workshop on Dependently typed programming (DTP'13), Sept 2013, Boston, USA, co-located with ICFP'13.
• 2nd ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE'13), Sept 2013, Boston, USA, co-located with ICFP'13.
• 24th International Joint Conference on Automated Deduction (CADE-24), Lake Placid, USA, June 2013
• International Conference on Interactive Theorem Proving (ITP'13), Rennes, France, Aug 2013

Professional Organizations

• I am on the SC of POPL (2017 - 2020).
• I am on the SC of (European Symposium on Programming Languages)( 2017 - 2020).
• I am on the SC of FSCD (Formal Structures for Computation and Deduction)(2016 - 2019).
• Elected Trustee of Conference of Automated Deduction (CADE) (elected in 2011, reelected in 2013)
• Steering Committee of Logical Frameworks and Meta-Languages (LFMTP)