|
|
[1]
|
Pientka, B.
A type-theoretic foundation for programming with higher-order
abstract syntax and first-class substitutions.
In 35th ACM Symposium on Principles of Programming Languages
(POPL'08),. ACM Press, January 2008, pp. 371-382.
|
|
[2]
|
Pientka, B., and Dunfield, J.
Programming with proofs and explicit contexts.
In ACM SIGPLAN Symposium on Principles and Practice of
Declarative Programming (PPDP'08). ACM Press, July 2008, pp. 163-173.
|
|
[3]
|
Nanevski, A., Pfenning, F., and Pientka, B.
Contextual modal type theory.
ACM Transactions on Computational Logic, 2008, v. 9, n. 3,
pp. 1-49.
Nanevski:ICML05.
|
|
[4]
|
Pientka, B.
Higher-order term indexing using substitution trees.
ACM Transactions on Computational Logic, 2008, pp. 1-50.
Pientka:TOCL08 In Press.
|
|
[5]
|
Pientka, B.
A type-theoretic foundation for programming with higher-order
abstract syntax and first-class substitutions.
In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL'08). ACM, 2008, pp. 371-382.
Pientka:POPL08.
|
|
[6]
|
Pientka, B., and Dunfield, J.
Programming with proofs and explicit contexts.
July 2008, pp. 163-173.
Pientka:PPDP08.
|
|
[7]
|
Heilala, S., and Pientka, B.
Bidirectional decision procedures for the intuitionistic
propositional modal logic is4.
In Pfenning, F., editor, 21st International Conference on
Automated Deduction (CADE-21), Bremen, Germany, July 17-20, 2007. Springer,
2007, v. 4603 of Lecture Notes in Computer Science, Lecture Notes in
Computer Science, pp. 116-131.
[ http ]
|
|
[8]
|
Pientka, B.
Proof pearl: The power of higher-order encodings in the logical
framework LF.
In Schneider, K., and Brandt, J., editors, 20th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs'07),
Kaiserslautern, Germany. Springer, 2007, Lecture Notes in Computer Science
(LNCS 4732), pp. 246-261.
|
|
[9]
|
Pientka, B.
Functional programming with higher-order abstract syntax and explicit
substitutions.
Electronic Notes Theoritical Computer Science, 2007, v. 174,
n. 7, pp. 41-60.
[ http ]
|
|
[10]
|
Momigliano, A., and Pientka, B.
Proceeding of the international workshop on logical frameworks and
meta-languages: Theory and practice (lfmtp'06), seattle, wa, usa.
Electronic Notes Theoretical Computer Science(ENTCS), 2007, v.
174, n. 5, pp. 1-2.
[ http ]
|
|
[11]
|
Nanevski, A., Pfenning, F., and Pientka, B.
A contextual modal type theory.
ACM Transactions on Computational Logic, 2006, p. 56.
In Press.
|
|
[12]
|
Pientka, B.
Overcoming performance barriers: Efficient verification techniques
for logical frameworks.(invited tutorial).
In Etalle, S., and Truszczynski, M., editors, 22nd International
Conference Logic Programming (ICLP), Seattle, WA, USA. Springer, 2006,
Lecture Notes in Computer Science (LNCS) 4079, pp. 3-10.
|
|
[13]
|
Pientka, B.
Eliminating redundancy in higher-order unification: a lightweight
approach.
In Furbach, U., and Shankar, N., editors, 3rd International
Joint Conference on Automated Reasoning, Seattle, WA, USA. SPR, 2006,
pp. 362-377.
|
|
[14]
|
Pientka, B.
Functional programming with higher-order abstract syntax and explicit
substitutions.
In Programming Languages meets Program Verification (PLPV),
Seattle, USA. Elsevier, 2006, Electronic Notes in Theoretical Computer
Science (ENTCS), pp. 87-102.
|
|
[15]
|
Pientka, B., and Momigliano, A., editors.
Proceeding of the International Workshop on Logical Frameworks
and Meta-Languages: Theory and Practice, Seattle, WA, USA, August 2006,
Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier.
|
|
|
