Andreas Abel & Brigitte Pientka (2010):
Explicit substitutions for contextual type theory.
In: Karl Crary & Marino Miculan: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'10),
Electronic Proceedings in Theoretical Computer Science (EPTCS) 34,
doi:10.4204/EPTCS.34.3.
Andreas Abel & Brigitte Pientka (2011):
Higher-Order Dynamic Pattern Unification for Dependent Types and Records.
In: Luke Ong: 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11),
Lecture Notes in Computer Science.
Springer,
pp. to appear,
doi:10.1007/978-3-642-21691-6_5.
Mirna Bognar & Roel de Vrijer (2001):
A calculus of lambda calculus context.
Journal of Automated Reasoning 27(1),
pp. 29–59,
doi:10.1023/A:1010654904735.
Rowan Davies & Frank Pfenning (2001):
A modal analysis of staged computation.
Journal of the ACM 48(3),
pp. 555–604,
doi:10.1145/382780.382785.
Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003):
Theorem Proving Modulo.
Journal of Automated Reasoning 31(1),
pp. 33–72,
doi:10.1023/A:1027357912519.
Murdoch Gabbay (2007):
Hierarchical Nominal Terms and Their Theory of Rewriting.
In: B. Pientka & A. Momigliano: 1st International Workshop on Logical Frameworks and Meta-Languages (LFMTP'06) 174(5).
Electronic Notes Theorical Computer Science,
pp. 37–52,
doi:10.1016/j.entcs.2007.01.017.
Murdoch J. Gabbay & Stéphane Lengrand (2009):
The lambda-context calculus (extended version).
Information and Computation 207,
pp. 1369–1400,
doi:10.1016/j.ic.2009.06.004.
Herman Geuvers & G.I Jojgov (2002):
Open Proofs and Open Terms: a Basis for Interactive Logic.
In: Julian C. Bradfield: Proceedings of the 16th International on Computer Science Logic (CSL'03) Edinburgh, Scotland, UK, September 22-25,
Lecture Notes in Computer Science (LNCS 2471).
Springer,
pp. 537–552,
doi:10.1007/3-540-45793-3_36.
Fausto Giunchiglia (1993):
Contextual Reasoning.
Epistemologia 16,
pp. 145–164.
Fausto Giunchiglia & Luciano Serafini (1994):
Multilanguage Hierarchical Logics or: How we can do Without Modal Logics.
Artificial Intelligence 65(1),
pp. 29–70,
doi:10.1016/0004-3702(94)90037-X.
Robert Glück & Jesper Jørgensen (1995):
Efficient Multi-level Generating Extensions for Program Specialization.
In: Manuel V. Hermenegildo & S. Doaitse Swierstra: 7th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP'95),
Lecture Notes in Computer Science LNCS(982).
Springer,
pp. 259–278,
doi:10.1007/BFb0026825.
Robert Glück & Jesper Jørgensen (1996):
Fast Binding-Time Analysis for Multi-Level Specialization.
In: Dines Bjørner, Manfred Broy & Igor V. Pottosin: 2nd International Andrei Ershov Memorial Conference,
Lecture Notes in Computer Science LNCS(1181) 1181.
Springer,
pp. 261–272,
doi:10.1007/3-540-62064-8_22.
Robert Harper, Furio Honsell & Gordon Plotkin (1993):
A Framework for Defining Logics.
Journal of the ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008):
Contextual modal type theory.
ACM Transactions on Computational Logic 9(3),
pp. 1–49,
doi:10.1145/1352582.1352591.
Frank Pfenning (2007):
On a Logical Foundation for Explicit Substitutions.
In: Simona Ronchi Della Rocca: 8th International Conference on Typed Lambda Calculi and Applications (TLCA'07),
Lecture Notes in Computer Science 4583.
Springer,
pp. 1,
doi:10.1007/978-3-540-73228-0_1.
Brigitte Pientka (2008):
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 Press,
pp. 371–382,
doi:10.1145/1328438.1328483.
Brigitte Pientka & Joshua Dunfield (2010):
Beluga: a Framework for Programming and Reasoning with Deductive Systems (System Description).
In: Jürgen Giesl & Reiner Haehnle: 5th International Joint Conference on Automated Reasoning (IJCAR'10),
Lecture Notes in Artificial Intelligence (LNAI 6173),
pp. 15–21,
doi:10.1007/978-3-642-14203-1_2.
Brigitte Pientka & Frank Pfenning (2003):
Optimizing higher-order pattern unification.
In: F. Baader: 19th International Conference on Automated Deduction, Miami, USA,
Lecture Notes in Artificial Intelligence (LNAI) 2741.
Springer-Verlag,
pp. 473–487,
doi:10.1007/978-3-540-45085-6_40.
Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama & Atsushi Igarashi (2003):
Calculi of Meta-varaibles.
In: Matthias Baaz & Johann A. Makowsky: Proceedings of the 17th International on Computer Science Logic (CSL'03) Vienna, Austria, August 25-30,
Lecture Notes in Computer Science (LNCS 2803).
Springer,
pp. 484–497,
doi:10.1007/978-3-540-45220-1_39.
Antonis Stampoulis & Zhong Shao (2010):
VeriML: typed computation of logical terms inside a language with effects.
In: Paul Hudak & Stephanie Weirich: 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10).
ACM,
pp. 333–344,
doi:10.1145/1863543.1863591.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2002):
A Concurrent Logical Framework I: Judgments and Properties.
Technical Report CMU-CS-02-101.
Department of Computer Science, Carnegie Mellon University.
Yosihiro Yuse & Atsushi Igarashi (2006):
A modal type system for multi-level generating extensions with persistent code.
In: Annalisa Bossi & Michael J. Maher: 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'06).
ACM,
pp. 201–212,
doi:10.1145/1140335.1140360.
eptcs@eptcs.org