Brigitte Pientka

Proc. ACM Program. Lang., 2025

A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, 2025

Split Decisions: Explicit Contexts for Substructural Languages.

[BibT_eX]

[DOI]

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

2024

A Layered Approach to Intensional Analysis in Type Theory.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., December, 2024

Message-Observing Sessions.

[BibT_eX]

[DOI]

Ryan Kavanagh

Proc. ACM Program. Lang., 2024

Polymorphic Metaprogramming with Memory Management - An Adjoint Analysis of Metaprogramming.

[BibT_eX]

[DOI]

Junyoung Jang

CoRR, 2024

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming.

[BibT_eX]

[DOI]

CoRR, 2024

SAT-DIFF: A Tree Diffing Framework Using SAT Solving.

[BibT_eX]

[DOI]

CoRR, 2024

Adjoint Natural Deduction (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2024

Adjoint Natural Deduction.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

Modernizing SMT-Based Type Error Localization.

[BibT_eX]

[DOI]

Max Kopinsky

Xujie Si

Proceedings of the Formal Methods in Computer-Aided Design, 2024

Layered Modal Type Theory - Where Meta-programming Meets Intensional Analysis.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2024

2023

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity.

[BibT_eX]

[DOI]

Chuta Sano

Ryan Kavanagh

Proc. ACM Program. Lang., October, 2023

Normalization by evaluation for modal dependent type theory.

[BibT_eX]

[DOI]

Junyoung Jang

J. Funct. Program., 2023

Contextual Refinement Types.

[BibT_eX]

[DOI]

Antoine Gaulin

Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2023

Semi-Automation of Meta-Theoretic Proofs in Beluga.

[BibT_eX]

[DOI]

Johanna Schwartzentruber

Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2023

Layered Modal Type Theories.

[BibT_eX]

[DOI]

CoRR, 2023

Can ChatGPT Pass An Introductory Level Functional Language Programming Course?

[BibT_eX]

[DOI]

CoRR, 2023

Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students.

[BibT_eX]

[DOI]

Proceedings of the 54th ACM Technical Symposium on Computer Science Education, Volume 1, 2023

2022

Novice Type Error Diagnosis with Natural Language Models - Artifacts.

[BibT_eX]

[DOI]

Dataset, August, 2022

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types.

[BibT_eX]

[DOI]

Ulrich Schöpp

ACM Trans. Comput. Log., 2022

Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

A Categorical Normalization Proof for the Modal Lambda-Calculus.

[BibT_eX]

[DOI]

Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, 2022

An Investigation of Kripke-style Modal Type Theories.

[BibT_eX]

[DOI]

CoRR, 2022

Novice Type Error Diagnosis with Natural Language Models.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 20th Asian Symposium, 2022

2021

Moebius: Metaprogramming using Contextual Types - The stage where System F can pattern match on itself (Long Version).

[BibT_eX]

[DOI]

CoRR, 2021

Data Collection for the Learn-OCaml Programming Platform: Modelling How Students Develop Typed Functional Programs.

[BibT_eX]

[DOI]

Alana Ceci

Hanneli C. A. Tavante

Xujie Si

Proceedings of the SIGCSE '21: The 52nd ACM Technical Symposium on Computer Science Education, 2021

Harpoon: Mechanizing Metatheory Interactively - (System Description).

[BibT_eX]

[DOI]

Jacob Errington

Junyoung Jang

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Contextual Types, Explained: Invited Tutorial.

[BibT_eX]

[DOI]

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

A Modal Analysis of Metaprogramming, Revisited (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Semantical Analysis of Contextual Types.

[BibT_eX]

[DOI]

Ulrich Schöpp

Proceedings of the Foundations of Software Science and Computation Structures, 2020

2019

Teaching the art of functional programming using automated grading (experience report).

[BibT_eX]

[DOI]

Aliya Hameer

Proc. ACM Program. Lang., 2019

A case study in programming coinductive proofs: Howe's method.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

POPLMark reloaded: Mechanizing proofs by logical relations.

[BibT_eX]

[DOI]

J. Funct. Program., 2019

Cocon: Computation in Contextual Type Theory.

[BibT_eX]

[DOI]

CoRR, 2019

A Type Theory for Defining Logics and Proofs.

[BibT_eX]

[DOI]

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2018

Mechanizing proofs with logical relations - Kripke-style.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2018

Index-Stratified Types (Extended Version).

[BibT_eX]

[DOI]

Rohan Jacob-Rao

CoRR, 2018

Index-Stratified Types.

[BibT_eX]

[DOI]

Rohan Jacob-Rao

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

POPLMark reloaded: mechanizing logical relations proofs (invited talk).

[BibT_eX]

[DOI]

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017

Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga.

[BibT_eX]

[DOI]

Jonas Kaiser

Gert Smolka

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

LINCX: A Linear Logical Framework with First-Class Contexts.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

Programs Using Syntax with First-Class Binders.

[BibT_eX]

[DOI]

Francisco Ferreira

Proceedings of the Programming Languages and Systems, 2017

2016

Well-founded recursion with copatterns and sized types.

[BibT_eX]

[DOI]

J. Funct. Program., 2016

Universality of Proofs (Dagstuhl Seminar 16421).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2016

Mechanizing Proofs about Mendler-style Recursion.

[BibT_eX]

[DOI]

Rohan Jacob-Rao

Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

Indexed codata types.

[BibT_eX]

[DOI]

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - A Survey.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

An Open Challenge Problem Repository for Systems Supporting Binders.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, 2015

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks.

[BibT_eX]

[DOI]

CoRR, 2015

A Case Study on Logical Relations using Contextual Types.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, 2015

Well-Founded Recursion over Contextual Objects.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

Mechanizing Meta-Theory in Beluga (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2015

Inductive Beluga: Programming Proofs.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Unnesting of Copatterns.

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Bidirectional Elaboration of Dependently Typed Programs.

[BibT_eX]

[DOI]

Francisco Ferreira

Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, 2014

Fair reactive programming.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

2013

An insider's look at LF type reconstruction: everything you (n)ever wanted to know.

[BibT_eX]

[DOI]

J. Funct. Program., 2013

Copatterns: programming infinite structures by observations.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Compiling contextual objects: bringing higher-order abstract syntax to programmers.

[BibT_eX]

[DOI]

Francisco Ferreira

Stefan Monnier

Proceedings of the 7th Workshop on Programming languages meets program verification, 2013

First-class substitutions in contextual type theory.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Wellfounded recursion with copatterns: a unified approach to termination and productivity.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Programming Type-Safe Transformations Using Higher-Order Abstract Syntax.

[BibT_eX]

[DOI]

Olivier Savary Bélanger

Stefan Monnier

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Programming with binders and indexed data-types.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

Preface: Special Issue of Selected Extended Papers of CADE-22.

[BibT_eX]

[DOI]

Renate A. Schmidt

J. Autom. Reason., 2011

Intuitionistic Modal Logic and Applications (IMLA 2008).

[BibT_eX]

[DOI]

Valeria de Paiva

Inf. Comput., 2011

Multi-level Contextual Type Theory

[BibT_eX]

[DOI]

Mathieu Boespflug

Proceedings of the Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2011

Higher-Order Dynamic Pattern Unification for Dependent Types and Records.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

2010

Explicit Substitutions for Contextual Type Theory

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Beluga: Programming with Dependent Types, Contextual Data, and Contexts.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description).

[BibT_eX]

[DOI]

Jana Dunfield

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Programming Inductive Proofs - A New Approach Based on Contextual Types.

[BibT_eX]

[DOI]

Proceedings of the Verification, Induction, Termination Analysis, 2010

2009

Higher-order term indexing using substitution trees.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2009

2008

Contextual modal type theory.

[BibT_eX]

[DOI]

Aleksandar Nanevski

Frank Pfenning

ACM Trans. Comput. Log., 2008

Case Analysis of Higher-Order Data.

[BibT_eX]

[DOI]

Jana Dunfield

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

Programming with proofs and explicit contexts.

[BibT_eX]

[DOI]

Jana Dunfield

Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2008

A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

Preface.

[BibT_eX]

[DOI]

Carsten Schürmann

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

Focusing the Inverse Method for LF: A Preliminary Report.

[BibT_eX]

[DOI]

Xi Li

Florent Pompigne

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4.

[BibT_eX]

[DOI]

Samuli Heilala

Proceedings of the Automated Deduction, 2007

2006

Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages meets Program Verification, 2006

Preface.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 22nd International Conference, 2006

Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Verifying Termination and Reduction Properties about Higher-Order Logic Programs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Small Proof Witnesses for LF.

[BibT_eX]

[DOI]

Susmit Sarkar

Karl Crary

Proceedings of the Logic Programming, 21st International Conference, 2005

Tabling for Higher-Order Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2003

Higher-Order Substitution Tree Indexing.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 19th International Conference, 2003

A modal foundation for meta-variables.

[BibT_eX]

[DOI]

Aleksandar Nanevski

Frank Pfenning

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Optimizing Higher-Order Pattern Unification.

[BibT_eX]

[DOI]

Frank Pfenning

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 18th International Conference, 2002

2001

Connection-Driven Inductive Theorem Proving.

[BibT_eX]

[DOI]

Stud Logica, 2001

Termination and Reduction Checking for Higher-Order Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

Matrix-Based Inductive Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2000

Matrix-based Constructive Theorem Proving.

[BibT_eX]

Proceedings of the Intellectics and Computational Logic (to Wolfgang Bibel on the occasion of his 60th birthday), 2000

1999

Automating Inductive Specification Proofs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1999

1998

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

1997

Structured Incremental Proof Planning.

[BibT_eX]

[DOI]

Stefan Gerberding