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