Travelled to:1 × Austria
1 × Denmark
1 × Estonia
1 × India
1 × Japan
1 × Poland
1 × Serbia
2 × Germany
2 × Italy
2 × Spain
2 × United Kingdom
7 × USA
Collaborated with:∅ A.Abel A.Cave J.Dunfield F.Ferreira A.Setzer D.Thibodeau S.Heilala F.Pfenning F.F.0001 S.Sarkar K.Crary P.Panangaden A.L.Georges A.Murawska S.Otis
Talks about:program (13) higher (8) order (8) logic (6) type (5) proof (4) framework (3) copattern (3) context (3) depend (3)
Person: Brigitte Pientka
DBLP: Pientka:Brigitte
Facilitated 1 volumes:
EdContributed to:
2015
2015
20142014
2014
2013201320122011
2010
2010200820082007
20062006200520052003200320022001
2017Wrote 24 papers:
- CADE-2015-PientkaC #induction #programming #proving
- Inductive Beluga: Programming Proofs (BP, AC), pp. 272–281.
- TLCA-2015-Pientka0 #recursion
- Well-Founded Recursion over Contextual Objects (BP, AA), pp. 273–287.
- POPL-2014-CaveFPP #programming
- Fair reactive programming (AC, FF, PP, BP), pp. 361–372.
- PPDP-2014-FerreiraP #bidirectional #source code
- Bidirectional Elaboration of Dependently Typed Programs (FF, BP), pp. 161–174.
- RTA-TLCA-2014-Setzer0PT #pattern matching
- Unnesting of Copatterns (AS, AA, BP, DT), pp. 31–45.
- ICFP-2013-AbelP #approach #pattern matching #recursion #termination
- Wellfounded recursion with copatterns: a unified approach to termination and productivity (AA, BP), pp. 185–196.
- POPL-2013-AbelPTS #infinity #named #pattern matching #programming
- Copatterns: programming infinite structures by observations (AA, BP, DT, AS), pp. 27–38.
- POPL-2012-CaveP #data type #programming
- Programming with binders and indexed data-types (AC, BP), pp. 413–424.
- TLCA-2011-AbelP #dependent type #higher-order #unification
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
- FLOPS-2010-Pientka #dependent type #named #programming
- Beluga: Programming with Dependent Types, Contextual Data, and Contexts (BP), pp. 1–12.
- IJCAR-2010-PientkaD #deduction #framework #named #programming #reasoning
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (BP, JD), pp. 15–21.
- POPL-2008-Pientka #higher-order #programming #syntax
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (BP), pp. 371–382.
- PPDP-2008-PientkaD #programming #proving
- Programming with proofs and explicit contexts (BP, JD), pp. 163–173.
- CADE-2007-HeilalaP #bidirectional #logic
- Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 (SH, BP), pp. 116–131.
- ICLP-2006-Pientka #framework #logic #performance #verification
- Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks (BP), pp. 3–10.
- IJCAR-2006-Pientka #approach #higher-order #lightweight #unification
- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach (BP), pp. 362–376.
- CADE-2005-Pientka #higher-order #logic programming
- Tabling for Higher-Order Logic Programming (BP), pp. 54–68.
- ICLP-2005-SarkarPC #proving
- Small Proof Witnesses for LF (SS, BP, KC), pp. 387–401.
- CADE-2003-PientkaP #higher-order #optimisation #unification
- Optimizing Higher-Order Pattern Unification (BP, FP), pp. 473–487.
- ICLP-2003-Pientka #higher-order
- Higher-Order Substitution Tree Indexing (BP), pp. 377–391.
- ICLP-2002-Pientka #higher-order #logic programming
- A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming (BP), pp. 271–286.
- IJCAR-2001-Pientka #higher-order #logic programming #reduction #source code #termination
- Termination and Reduction Checking for Higher-Order Logic Programs (BP), pp. 401–415.
- ESOP-2017-0001P #source code #syntax #using
- Programs Using Syntax with First-Class Binders (FF0, BP), pp. 504–529.
- ESOP-2017-GeorgesMOP #framework #linear #logic #named
- LINCX: A Linear Logical Framework with First-Class Contexts (ALG, AM, SO, BP), pp. 530–555.