News and Upcoming Events

• I am on sabbatical and have been awarded a Humboldt Fellowship to visit the MPI-SWS, Germany!
• I am the PC chair ICFP in 2024
• I am co-PC chair for CPP in 2023 and 2024
• I am on the PC for POPL'23
• I am on the PC for IJCAR'22
• I am on the PC for TYPES'22
• I am on the PC for CPP'22
• I am on the SC of LICS (Logic in Computer Science)
• I am one of the executive editors of the diamond open-access journal, Logical Methods in Computer Science
• I gave an invited talk at FSCD'20
• I gave an invited tutorial talk at LICS'20
• 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 a PPDP'18 (slides)!
• I am the general chair of POPL 2020.
• 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

• Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction (Extended Version), Feb 2024
• Jason Z.S. Hu and Brigitte Pientka. Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis, 33rd European Symposium on Programming (ESOP'24)
• Ryan Kavanagh and Brigitte Pientka. Message-Observing Sessions, accepted at OOPSLA'24.
• Chuta Sano and Ryan Kavanagh and Brigitte Pientka. Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity, OOPSLA'2023, Oct 2023
• Jason Z.S. Hu and Junyoung Jang and Brigitte Pientka. Normalization by evaluation for modal dependent type theory, Journal of Functional Programming (JFP), Oct 2023
• Antoine Gaulin and Brigitte Pientka. Contextual Refinement Types, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23), July 2023
• Johanna Schwartzentruber and Brigitte Pientka. Semi-Automation of Meta-Theoretic Proofs in Beluga, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'23), July 2023
• Chuqin Geng, Wenwen Xu, Yingjie Xu, Brigitte Pientka, Xujie Si. Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students. 54th ACM Technical Symposium on Computer Science Education (SIGCSE - Vol 1) 2023
• Jason Z.S. Hu and Brigitte Pientka. A Categorical Normalization Proof for the Modal Lambda-Calculus, 38th International Conference on Mathematical Foundations of Programming Semantics (MFPS 2022)
• Jason Z.S. Hu and Brigitte Pientka, and Ulrich Schoepp. A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types, ACM Transactions of Computational Logic (TOCL) (doi, July 2022
• Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka, Moebius: Metaprogramming using contextual types-- the stage where System F can pattern match on itself, POPL 2022
• Jacob Errington, Junyoung Jang, Brigitte Pientka, Harpoon: Mechanizing Metatheory Interactively - (System Description), CADE 2021
• 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
• Alberto Momigliano, Brigitte Pientka, David Thibodeau: A case study in programming coinductive proofs: Howe's method. Math. Struct. Comput. Sci. 29(8): 1309-1343 (2019)
• Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, Kathrin Stark: POPLMark Reloaded: Mechanizing Logical Relations Proofs, J. Funct. Program. 29:(e19), 2019
• 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.

For a list of all publications see Research.

Recent Drafts

• Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rebecca Zuccini, Cocon: Computation in Contextual Type Theory, Extended Technical Report, Jan 2019
• 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 (selected)

• Mechanizing Session-Types: Enforcing linearity without linearity, 18th International Workshop on Logical and Semantic Frameworks, with Applications, LFSA'23, July 2023
• A Modal Analysis of Dependently-Typed Meta-Programming, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'22) (Special Session in Honor of Frank Pfenning), July 2022
• 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

• International Conference on Functional Programming (ICFP'24)
• Certified Proofs and Programs (CPP'24)
• International Conference on Automated Deduction (CADE'23)
• Certified Proofs and Programs (CPP'23)
• 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

• Executive Editor of Logical Methods in Computer Science
• 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

• 50th ACM Symposium on Principles of Programming Languages (POPL'23)
• 11th International Joint Conference on Automated Reasoning (IJCAR 2022)
• 28th International Conference on Types for Proofs and Programs (TYPES'22)
• 11th International Conference on Certified Programs and Proofs (CPP'22)
• 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

Professional Organizations

• I am on the SC of LICS (2021).
• 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)