| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Andrew Cave, Brigitte Pientka |
Programming with binders and indexed data-types.  |
POPL  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Valeria de Paiva, Brigitte Pientka |
Intuitionistic Modal Logic and Applications (IMLA 2008). |
Inf. Comput. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathieu Boespflug, Brigitte Pientka |
Multi-level Contextual Type Theory |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Renate A. Schmidt, Brigitte Pientka |
Preface: Special Issue of Selected Extended Papers of CADE-22. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Brigitte Pientka |
Higher-Order Dynamic Pattern Unification for Dependent Types and Records. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Brigitte Pientka |
Explicit Substitutions for Contextual Type Theory |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Joshua Dunfield |
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). |
IJCAR |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Brigitte Pientka |
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Beluga: Programming with Dependent Types, Contextual Data, and Contexts. |
FLOPS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Programming Inductive Proofs - A New Approach Based on Contextual Types. |
Verification, Induction, Termination Analysis |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua Dunfield, Brigitte Pientka |
Case Analysis of Higher-Order Data. |
Electr. Notes Theor. Comput. Sci. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Higher-order term indexing using substitution trees. |
ACM Trans. Comput. Log. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Carsten Schürmann |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Xi Li, Florent Pompigne |
Focusing the Inverse Method for LF: A Preliminary Report. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka |
Contextual modal type theory. |
ACM Trans. Comput. Log. |
2008 |
DBLP DOI BibTeX RDF |
intuitionistic modal logic, Type theory, logical frameworks |
| 1 | Brigitte Pientka |
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. |
POPL |
2008 |
DBLP DOI BibTeX RDF |
type system, logical frameworks |
| 1 | Brigitte Pientka, Joshua Dunfield |
Programming with proofs and explicit contexts. |
PPDP |
2008 |
DBLP DOI BibTeX RDF |
type theory, dependent types, logical frameworks |
| 1 | Brigitte Pientka |
Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Momigliano, Brigitte Pientka |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Samuli Heilala, Brigitte Pientka |
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks. |
ICLP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Verifying Termination and Reduction Properties about Higher-Order Logic Programs. |
J. Autom. Reasoning |
2005 |
DBLP DOI BibTeX RDF |
termination, Logical frameworks |
| 1 | Brigitte Pientka |
Tabling for Higher-Order Logic Programming. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Susmit Sarkar, Brigitte Pientka, Karl Crary |
Small Proof Witnesses for LF. |
ICLP |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Frank Pfenning |
Optimizing Higher-Order Pattern Unification. |
CADE |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Higher-Order Substitution Tree Indexing. |
ICLP |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning |
A modal foundation for meta-variables. |
MERLIN |
2003 |
DBLP DOI BibTeX RDF |
modal type theory, pattern unification, logical frameworks |
| 1 | Brigitte Pientka |
Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. |
ICLP |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Kreitz, Brigitte Pientka |
Connection-Driven Inductive Theorem Proving. |
Studia Logica |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Termination and Reduction Checking for Higher-Order Logic Programs. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Kreitz, Brigitte Pientka |
Matrix-Based Inductive Theorem Proving. |
TABLEAUX |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka |
Matrix-based Constructive Theorem Proving. |
Intellectics and Computational Logic |
2000 |
DBLP BibTeX RDF |
|
| 1 | Brigitte Pientka, Christoph Kreitz |
Automating Inductive Specification Proofs. |
Fundam. Inform. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Christoph Kreitz |
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Gerberding, Brigitte Pientka |
Structured Incremental Proof Planning. |
KI |
1997 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")