default search action
Search dblp for Publications
export results for "stream:conf/lfmtp:"
@inproceedings{DBLP:journals/corr/abs-2407-06624, author = {Gabriele Cecilia and Alberto Momigliano}, editor = {Florian Rabe and Claudio Sacerdoti Coen}, title = {A Beluga Formalization of the Harmony Lemma in the {\(\pi\)}-Calculus}, booktitle = {Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024}, series = {{EPTCS}}, volume = {404}, pages = {1--17}, year = {2024}, url = {https://doi.org/10.4204/EPTCS.404.1}, doi = {10.4204/EPTCS.404.1}, timestamp = {Wed, 04 Sep 2024 16:17:48 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2407-06624.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2407-06625, author = {Terrance Gray and Gopalan Nadathur}, editor = {Florian Rabe and Claudio Sacerdoti Coen}, title = {Binding Contexts as Partitionable Multisets in Abella}, booktitle = {Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024}, series = {{EPTCS}}, volume = {404}, pages = {19--34}, year = {2024}, url = {https://doi.org/10.4204/EPTCS.404.2}, doi = {10.4204/EPTCS.404.2}, timestamp = {Wed, 04 Sep 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2407-06625.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2407-06626, author = {Thomas Traversi{\'{e}}}, editor = {Florian Rabe and Claudio Sacerdoti Coen}, title = {Kuroda's Translation for the {\(\lambda\)}{\(\pi\)}-Calculus Modulo Theory and Dedukti}, booktitle = {Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024}, series = {{EPTCS}}, volume = {404}, pages = {35--48}, year = {2024}, url = {https://doi.org/10.4204/EPTCS.404.3}, doi = {10.4204/EPTCS.404.3}, timestamp = {Wed, 04 Sep 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2407-06626.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2407-06627, author = {Thomas Traversi{\'{e}}}, editor = {Florian Rabe and Claudio Sacerdoti Coen}, title = {Proofs for Free in the {\(\lambda\)}{\(\pi\)}-Calculus Modulo Theory}, booktitle = {Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024}, series = {{EPTCS}}, volume = {404}, pages = {49--63}, year = {2024}, url = {https://doi.org/10.4204/EPTCS.404.4}, doi = {10.4204/EPTCS.404.4}, timestamp = {Wed, 04 Sep 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2407-06627.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-2407-05822, editor = {Florian Rabe and Claudio Sacerdoti Coen}, title = {Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024}, series = {{EPTCS}}, volume = {404}, year = {2024}, url = {https://doi.org/10.4204/EPTCS.404}, doi = {10.4204/EPTCS.404}, timestamp = {Wed, 04 Sep 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2407-05822.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10439, author = {Johanna Schwartzentruber and Brigitte Pientka}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Semi-Automation of Meta-Theoretic Proofs in Beluga}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {20--35}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.3}, doi = {10.4204/EPTCS.396.3}, timestamp = {Fri, 22 Dec 2023 16:43:30 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10439.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10440, author = {James T. Oswald and Brandon Rozek}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Parallel Verification of Natural Deduction Proof Graphs}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {36--51}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.4}, doi = {10.4204/EPTCS.396.4}, timestamp = {Sun, 04 Aug 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10440.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10577, author = {Antoine Gaulin and Brigitte Pientka}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Contextual Refinement Types}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {4--19}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.2}, doi = {10.4204/EPTCS.396.2}, timestamp = {Fri, 22 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10577.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2311-10578, author = {F{\'{e}}lix Castro}, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {An Interpretation of E-HA\({}^{\mbox{w}}\) inside HA\({}^{\mbox{w}}\)}, booktitle = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, pages = {52--66}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396.5}, doi = {10.4204/EPTCS.396.5}, timestamp = {Fri, 22 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-10578.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-2311-09918, editor = {Alberto Ciaffaglione and Carlos Olarte}, title = {Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023}, series = {{EPTCS}}, volume = {396}, year = {2023}, url = {https://doi.org/10.4204/EPTCS.396}, doi = {10.4204/EPTCS.396}, timestamp = {Fri, 22 Dec 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2311-09918.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07661, author = {Giselle Reis}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Facilitating Meta-Theory Reasoning (Invited Paper)}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {1--12}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.1}, doi = {10.4204/EPTCS.337.1}, timestamp = {Mon, 26 Jun 2023 20:50:02 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07661.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07662, author = {Gilles Dowek}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Interacting Safely with an Unsafe Environment}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {30--38}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.3}, doi = {10.4204/EPTCS.337.3}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07662.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07663, author = {Qinxiang Cao and Xiwei Wu}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Countability of Inductive Types Formalized in the Object-Logic Level}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {55--70}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.5}, doi = {10.4204/EPTCS.337.5}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07663.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07664, author = {Laila El{-}Beheiry and Giselle Reis and Ammar Karkour}, editor = {Elaine Pimentel and Enrico Tassi}, title = {SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from {SML} Programs with Contracts}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {71--87}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.6}, doi = {10.4204/EPTCS.337.6}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07664.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07665, author = {Florian Rabe and Navid Roux}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {88--103}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.7}, doi = {10.4204/EPTCS.337.7}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07665.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07666, author = {Mary Southern and Gopalan Nadathur}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Adelfa: {A} System for Reasoning about {LF} Specifications}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {104--120}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.8}, doi = {10.4204/EPTCS.337.8}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07666.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07669, author = {Johannes Schoisswohl and Laura Kov{\'{a}}cs}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Automating Induction by Reflection}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {39--54}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.4}, doi = {10.4204/EPTCS.337.4}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07669.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-07670, author = {Matthieu Sozeau}, editor = {Elaine Pimentel and Enrico Tassi}, title = {Touring the MetaCoq Project (Invited Paper)}, booktitle = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, pages = {13--29}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337.2}, doi = {10.4204/EPTCS.337.2}, timestamp = {Mon, 29 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07670.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-2101-02835, editor = {Claudio Sacerdoti Coen and Alwen Tiu}, title = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020}, series = {{EPTCS}}, volume = {332}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.332}, doi = {10.4204/EPTCS.332}, timestamp = {Tue, 02 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2101-02835.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-2107-07376, editor = {Elaine Pimentel and Enrico Tassi}, title = {Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2021, Pittsburgh, USA, 16th July 2021}, series = {{EPTCS}}, volume = {337}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.337}, doi = {10.4204/EPTCS.337}, timestamp = {Mon, 26 Jun 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-07376.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2101-03807, author = {Arve Gengelbach and Johannes {\AA}man Pohjola and Tjark Weber}, editor = {Claudio Sacerdoti Coen and Alwen Tiu}, title = {Mechanisation of Model-theoretic Conservative Extension for {HOL} with Ad-hoc Overloading}, booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020}, series = {{EPTCS}}, volume = {332}, pages = {1--17}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.332.1}, doi = {10.4204/EPTCS.332.1}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2101-03807.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2101-03808, author = {Petros Papapanagiotou and Jacques D. Fleuriot}, editor = {Claudio Sacerdoti Coen and Alwen Tiu}, title = {Object-Level Reasoning with Logics Encoded in {HOL} Light}, booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020}, series = {{EPTCS}}, volume = {332}, pages = {18--34}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.332.2}, doi = {10.4204/EPTCS.332.2}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2101-03808.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2101-03809, author = {Tarmo Uustalu and Niccol{\`{o}} Veltri and Noam Zeilberger}, editor = {Claudio Sacerdoti Coen and Alwen Tiu}, title = {Deductive Systems and Coherence for Skew Prounital Closed Categories}, booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020}, series = {{EPTCS}}, volume = {332}, pages = {35--53}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.332.3}, doi = {10.4204/EPTCS.332.3}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2101-03809.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2101-03810, author = {Bruno Barras and Valentin Maestracci}, editor = {Claudio Sacerdoti Coen and Alwen Tiu}, title = {Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory}, booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020}, series = {{EPTCS}}, volume = {332}, pages = {54--67}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.332.4}, doi = {10.4204/EPTCS.332.4}, timestamp = {Tue, 02 Feb 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2101-03810.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1910-10848, author = {Fabio Alessi and Alberto Ciaffaglione and Pietro Di Gianantonio and Furio Honsell and Marina Lenisa}, editor = {Dale Miller and Ivan Scagnetto}, title = {A Definitional Implementation of the Lax Logical Framework {LLFP} in Coq, for Supporting Fast and Loose Reasoning}, booktitle = {Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019}, series = {{EPTCS}}, volume = {307}, pages = {8--23}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.307.3}, doi = {10.4204/EPTCS.307.3}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1910-10848.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1910-10849, author = {Michael Kohlhase and Jan Frederik Schaefer}, editor = {Dale Miller and Ivan Scagnetto}, title = {{GF} + {MMT} = {GLF} - From Language to Semantics through {LF}}, booktitle = {Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019}, series = {{EPTCS}}, volume = {307}, pages = {24--39}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.307.4}, doi = {10.4204/EPTCS.307.4}, timestamp = {Mon, 11 Nov 2019 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1910-10849.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1910-10850, author = {Dennis M{\"{u}}ller and Florian Rabe}, editor = {Dale Miller and Ivan Scagnetto}, title = {Rapid Prototyping Formal Systems in {MMT:} 5 Case Studies}, booktitle = {Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019}, series = {{EPTCS}}, volume = {307}, pages = {40--54}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.307.5}, doi = {10.4204/EPTCS.307.5}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1910-10850.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1910-10851, author = {Aaron Stump}, editor = {Dale Miller and Ivan Scagnetto}, title = {A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille}, booktitle = {Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019}, series = {{EPTCS}}, volume = {307}, pages = {55--67}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.307.6}, doi = {10.4204/EPTCS.307.6}, timestamp = {Mon, 11 Nov 2019 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1910-10851.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1910-08712, editor = {Dale Miller and Ivan Scagnetto}, title = {Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019}, series = {{EPTCS}}, volume = {307}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.307}, doi = {10.4204/EPTCS.307}, timestamp = {Mon, 11 Nov 2019 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1910-08712.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1807-01869, author = {Carlo Angiuli and Evan Cavallo and Kuen{-}Bang Hou (Favonia) and Robert Harper and Jonathan Sterling}, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {The RedPRL Proof Assistant (Invited Paper)}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, pages = {1--10}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274.1}, doi = {10.4204/EPTCS.274.1}, timestamp = {Thu, 22 Sep 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01869.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1807-01870, author = {Ernesto Copello and Nora Szasz and {\'{A}}lvaro Tasistro}, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, pages = {11--26}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274.2}, doi = {10.4204/EPTCS.274.2}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01870.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1807-01871, author = {Mart{\'{\i}}n Copes and Nora Szasz and {\'{A}}lvaro Tasistro}, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, pages = {27--41}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274.3}, doi = {10.4204/EPTCS.274.3}, timestamp = {Sat, 30 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01871.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1807-01872, author = {Rodolphe Lepigre and Christophe Raffalli}, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {Abstract Representation of Binders in OCaml using the Bindlib Library}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, pages = {42--56}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274.4}, doi = {10.4204/EPTCS.274.4}, timestamp = {Mon, 10 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01872.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1807-01873, author = {Fran{\c{c}}ois Thir{\'{e}}}, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {Sharing a Library between Proof Assistants: Reaching out to the {HOL} Family}, booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, pages = {57--71}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274.5}, doi = {10.4204/EPTCS.274.5}, timestamp = {Mon, 10 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01873.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1807-01352, editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis}, title = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018}, series = {{EPTCS}}, volume = {274}, year = {2018}, url = {https://doi.org/10.4204/EPTCS.274}, doi = {10.4204/EPTCS.274}, timestamp = {Mon, 10 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1807-01352.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/BattellF16, author = {Chelsea Battell and Amy P. Felty}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {3:1--3:10}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966271}, doi = {10.1145/2966268.2966271}, timestamp = {Tue, 06 Nov 2018 16:57:31 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/BattellF16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Breitner16, author = {Joachim Breitner}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {The Incredible Proof Machine (Invited Talk)}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {5:1}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966273}, doi = {10.1145/2966268.2966273}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Breitner16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Cauderlier16, author = {Rapha{\"{e}}l Cauderlier}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {A Rewrite System for Proof Constructivization}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {2:1--2:7}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966270}, doi = {10.1145/2966268.2966270}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Cauderlier16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/DunchevCT16, author = {Cvetan Dunchev and Claudio Sacerdoti Coen and Enrico Tassi}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {Implementing {HOL} in an Higher Order Logic Programming Language}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {4:1--4:10}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966272}, doi = {10.1145/2966268.2966272}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/DunchevCT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Jacob-RaoCP16, author = {Rohan Jacob{-}Rao and Andrew Cave and Brigitte Pientka}, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {Mechanizing Proofs about Mendler-style Recursion}, booktitle = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, pages = {1:1--1:9}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268.2966269}, doi = {10.1145/2966268.2966269}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Jacob-RaoCP16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2016, editor = {Gilles Dowek and Daniel R. Licata and Sandra Alves}, title = {Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} 2016, Porto, Portugal, June 23, 2016}, publisher = {{ACM}}, year = {2016}, url = {https://doi.org/10.1145/2966268}, doi = {10.1145/2966268}, isbn = {978-1-4503-4777-8}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2016.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/CaveP15, author = {Andrew Cave and Brigitte Pientka}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {A Case Study on Logical Relations using Contextual Types}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {33--45}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.3}, doi = {10.4204/EPTCS.185.3}, timestamp = {Wed, 12 Sep 2018 01:05:12 +0200}, biburl = {https://dblp.org/rec/journals/corr/CaveP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/FeltyMP15a, author = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {An Open Challenge Problem Repository for Systems Supporting Binders}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {18--32}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.2}, doi = {10.4204/EPTCS.185.2}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/FeltyMP15a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/GuenotG15, author = {Nicolas Guenot and Daniel Gustafsson}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {Sequent Calculus and Equational Programming}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {102--109}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.7}, doi = {10.4204/EPTCS.185.7}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/GuenotG15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/HonsellLMS15, author = {Furio Honsell and Luigi Liquori and Petar Maksimovic and Ivan Scagnetto}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {Gluing together Proof Environments: Canonical extensions of {LF} Type Theories featuring Locks}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {3--17}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.1}, doi = {10.4204/EPTCS.185.1}, timestamp = {Mon, 26 Oct 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/HonsellLMS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/PereraC15, author = {Roly Perera and James Cheney}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {Proof-relevant pi-calculus}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {46--70}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.4}, doi = {10.4204/EPTCS.185.4}, timestamp = {Wed, 07 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/PereraC15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/Saillard15, author = {Ronan Saillard}, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {Rewriting Modulo {\(\beta\)}in the {\(\lambda\)}{\(\Pi\)}-Calculus Modulo}, booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, pages = {87--101}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185.6}, doi = {10.4204/EPTCS.185.6}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/Saillard15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/CervesatoC15, editor = {Iliano Cervesato and Kaustuv Chaudhuri}, title = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, {LFMTP} 2015, Berlin, Germany, 1 August 2015}, series = {{EPTCS}}, volume = {185}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.185}, doi = {10.4204/EPTCS.185}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/CervesatoC15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/AltenkirchLR14, author = {Thorsten Altenkirch and Nuo Li and Ondrej Rypacek}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Some constructions on {\(\omega\)}-groupoids}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {4: 1--4: 8}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631176}, doi = {10.1145/2631172.2631176}, timestamp = {Sun, 02 Jun 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/AltenkirchLR14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/AnandR14, author = {Abhishek Anand and Vincent Rahli}, editor = {Amy P. Felty and Brigitte Pientka}, title = {A Generic Approach to Proofs about Substitution}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {5: 1--5: 8}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631177}, doi = {10.1145/2631172.2631177}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/AnandR14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/BelangerC14, author = {Olivier Savary B{\'{e}}langer and Kaustuv Chaudhuri}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Automatically Deriving Schematic Theorems for Dynamic Contexts}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {9: 1--9: 8}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631181}, doi = {10.1145/2631172.2631181}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/BelangerC14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Bengtson14, author = {Jesper Bengtson}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Session Types Meet Separation Logic}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {1: 1}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631173}, doi = {10.1145/2631172.2631173}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Bengtson14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Brady14, author = {Edwin C. Brady}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Idris: Implementing a Dependently Typed Programming Language}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {2: 1}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631174}, doi = {10.1145/2631172.2631174}, timestamp = {Sun, 21 Jun 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/Brady14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Brock-Nannestad14, author = {Taus Brock{-}Nannestad and Nicolas Guenot and Agata Murawska and Carsten Sch{\"{u}}rmann}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Hybrid Extensions in a Logical Framework}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {6: 1--6: 8}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631178}, doi = {10.1145/2631172.2631178}, timestamp = {Tue, 30 Jan 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Brock-Nannestad14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Cervesato14, author = {Iliano Cervesato}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Proof-Theoretic Foundations of Indexing in Logic Programming}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {7: 1--7: 9}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631179}, doi = {10.1145/2631172.2631179}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Cervesato14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/CiaffaglioneS14, author = {Alberto Ciaffaglione and Ivan Scagnetto}, editor = {Amy P. Felty and Brigitte Pientka}, title = {Internal Adequacy of Bookkeeping in Coq}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {8: 1--8: 8}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631180}, doi = {10.1145/2631172.2631180}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/CiaffaglioneS14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Nadathur14, author = {Gopalan Nadathur}, editor = {Amy P. Felty and Brigitte Pientka}, title = {A Framework for the Verified Transformation of Functional Programs}, booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, pages = {3: 1}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172.2631175}, doi = {10.1145/2631172.2631175}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Nadathur14.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2014, editor = {Amy P. Felty and Brigitte Pientka}, title = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014}, publisher = {{ACM}}, year = {2014}, url = {https://doi.org/10.1145/2631172}, doi = {10.1145/2631172}, isbn = {978-1-4503-2817-3}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2014.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/CaveP13, author = {Andrew Cave and Brigitte Pientka}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {First-class substitutions in contextual type theory}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {15--24}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503889}, doi = {10.1145/2503887.2503889}, timestamp = {Tue, 06 Nov 2018 16:57:31 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/CaveP13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/DoornGW13, author = {Floris van Doorn and Herman Geuvers and Freek Wiedijk}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Explicit convertibility proofs in pure type systems}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {25--36}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503890}, doi = {10.1145/2503887.2503890}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/DoornGW13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/FarooqueGM13, author = {Mahfuza Farooque and St{\'{e}}phane Graham{-}Lengrand and Assia Mahboubi}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {A bisimulation between DPLL(\emph{T}) and a proof-search strategy for the focused sequent calculus}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {3--14}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503892}, doi = {10.1145/2503887.2503892}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/FarooqueGM13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Honsell13, author = {Furio Honsell}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {25 years of formal proof cultures: some problems, some philosophy, bright future}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {37--42}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503896}, doi = {10.1145/2503887.2503896}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Honsell13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Miller13, author = {Dale Miller}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Foundational proof certificates: making proof universal and permanent}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {1--2}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503894}, doi = {10.1145/2503887.2503894}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Miller13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/RasmussenF13, author = {Ulrik Terp Rasmussen and Andrzej Filinski}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Structural logical relations with case analysis and equality reasoning}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {43--54}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503891}, doi = {10.1145/2503887.2503891}, timestamp = {Sat, 28 Aug 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/RasmussenF13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/WangN13, author = {Yuting Wang and Gopalan Nadathur}, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Towards extracting explicit proofs from totality checking in twelf}, booktitle = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, pages = {55--66}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887.2503893}, doi = {10.1145/2503887.2503893}, timestamp = {Sun, 25 Jul 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/WangN13.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2013, editor = {Alberto Momigliano and Brigitte Pientka and Randy Pollack}, title = {Proceedings of the Eighth {ACM} {SIGPLAN} International Workshop on Logical Frameworks {\&} Meta-languages: Theory {\&} Practice, {LFMTP} 2013, Boston, Massachusetts, USA, September 23, 2013}, publisher = {{ACM}}, year = {2013}, url = {https://doi.org/10.1145/2503887}, doi = {10.1145/2503887}, isbn = {978-1-4503-2382-6}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2013.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0085, author = {Andreas Abel and Nicolai Kraus}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {A Lambda Term Representation Inspired by Linear Ordered Logic}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {1--13}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.1}, doi = {10.4204/EPTCS.71.1}, timestamp = {Fri, 02 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0085.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0086, author = {Maxime Beauquier and Carsten Sch{\"{u}}rmann}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {A Bigraph Relational Model}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {14--28}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.2}, doi = {10.4204/EPTCS.71.2}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0086.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0087, author = {Mathieu Boespflug and Brigitte Pientka}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {Multi-level Contextual Type Theory}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {29--43}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.3}, doi = {10.4204/EPTCS.71.3}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0087.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0088, author = {Ranald Clouston}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {Nominal Logic with Equations Only}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {44--57}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.4}, doi = {10.4204/EPTCS.71.4}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0088.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0089, author = {Murdoch James Gabbay and Dominic P. Mulligan}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {58--75}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.5}, doi = {10.4204/EPTCS.71.5}, timestamp = {Mon, 26 Oct 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0089.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1111-0090, author = {Alan J. Martin and Amy P. Felty}, editor = {Herman Geuvers and Gopalan Nadathur}, title = {An Improved Implementation and Abstract Interface for Hybrid}, booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, pages = {76--90}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71.6}, doi = {10.4204/EPTCS.71.6}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1111-0090.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1110-6685, editor = {Herman Geuvers and Gopalan Nadathur}, title = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2011, Nijmegen, The Netherlands, August 26, 2011}, series = {{EPTCS}}, volume = {71}, year = {2011}, url = {https://doi.org/10.4204/EPTCS.71}, doi = {10.4204/EPTCS.71}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1110-6685.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2789, author = {Andreas Abel and Brigitte Pientka}, editor = {Karl Crary and Marino Miculan}, title = {Explicit Substitutions for Contextual Type Theory}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {5--20}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.3}, doi = {10.4204/EPTCS.34.3}, timestamp = {Mon, 05 Feb 2024 20:18:33 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2789.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2790, author = {John Tang Boyland}, editor = {Karl Crary and Marino Miculan}, title = {Generating Bijections between {HOAS} and the Natural Numbers}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {21--35}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.4}, doi = {10.4204/EPTCS.34.4}, timestamp = {Sun, 06 Oct 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2790.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2791, author = {Maribel Fern{\'{a}}ndez and Murdoch James Gabbay}, editor = {Karl Crary and Marino Miculan}, title = {Closed nominal rewriting and efficiently computable nominal algebra equality}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {37--51}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.5}, doi = {10.4204/EPTCS.34.5}, timestamp = {Mon, 26 Oct 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2791.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2792, author = {Herman Geuvers and Robbert Krebbers and James McKinna and Freek Wiedijk}, editor = {Karl Crary and Marino Miculan}, title = {Pure Type Systems without Explicit Contexts}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {53--67}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.6}, doi = {10.4204/EPTCS.34.6}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2792.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2793, author = {Daniel R. Licata and Robert Harper}, editor = {Karl Crary and Marino Miculan}, title = {A Monadic Formalization of {ML5}}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {69--83}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.7}, doi = {10.4204/EPTCS.34.7}, timestamp = {Fri, 02 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2793.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2794, author = {Florian Rabe}, editor = {Karl Crary and Marino Miculan}, title = {Representing Isabelle in {LF}}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {85--99}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.8}, doi = {10.4204/EPTCS.34.8}, timestamp = {Fri, 20 Nov 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2794.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1009-2795, author = {Anders Schack{-}Nielsen and Carsten Sch{\"{u}}rmann}, editor = {Karl Crary and Marino Miculan}, title = {Pattern Unification for the Lambda Calculus with Linear and Affine Types}, booktitle = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, pages = {101--116}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34.9}, doi = {10.4204/EPTCS.34.9}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2795.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1009-2189, editor = {Karl Crary and Marino Miculan}, title = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} 2010, Edinburgh, UK, 14th July 2010}, series = {{EPTCS}}, volume = {34}, year = {2010}, url = {https://doi.org/10.4204/EPTCS.34}, doi = {10.4204/EPTCS.34}, timestamp = {Mon, 05 Feb 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-1009-2189.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Adams09, author = {Robin Adams}, editor = {James Cheney and Amy P. Felty}, title = {Coercive subtyping in lambda-free logical frameworks}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {30--39}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577830}, doi = {10.1145/1577824.1577830}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Adams09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/BurelD09, author = {Guillaume Burel and Gilles Dowek}, editor = {James Cheney and Amy P. Felty}, title = {How can we prove that a proof search method is not an instance of another?}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {84--87}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577838}, doi = {10.1145/1577824.1577838}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/BurelD09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Crary09, author = {Karl Crary}, editor = {James Cheney and Amy P. Felty}, title = {A syntactic account of singleton types via hereditary substitution}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {21--29}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577829}, doi = {10.1145/1577824.1577829}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Crary09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/DoczkalS09, author = {Christian Doczkal and Jan Schwinghammer}, editor = {James Cheney and Amy P. Felty}, title = {Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {57--63}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577834}, doi = {10.1145/1577824.1577834}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/DoczkalS09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/GabbayM09, author = {Murdoch James Gabbay and Dominic P. Mulligan}, editor = {James Cheney and Amy P. Felty}, title = {Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {64--73}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577835}, doi = {10.1145/1577824.1577835}, timestamp = {Sun, 25 Oct 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/lfmtp/GabbayM09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/GunterOP09, author = {Elsa L. Gunter and Christopher J. Osborn and Andrei Popescu}, editor = {James Cheney and Amy P. Felty}, title = {Theory support for weak higher order abstract syntax in Isabelle/HOL}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {12--20}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577827}, doi = {10.1145/1577824.1577827}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/GunterOP09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Howe09, author = {Douglas J. Howe}, editor = {James Cheney and Amy P. Felty}, title = {Higher-order abstract syntax in classical higher-order logic}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {1--11}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577826}, doi = {10.1145/1577824.1577826}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Howe09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/RabeS09, author = {Florian Rabe and Carsten Sch{\"{u}}rmann}, editor = {James Cheney and Amy P. Felty}, title = {A practical module system for {LF}}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {40--48}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577831}, doi = {10.1145/1577824.1577831}, timestamp = {Fri, 20 Nov 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/RabeS09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/Reed09, author = {Jason Reed}, editor = {James Cheney and Amy P. Felty}, title = {Higher-order constraint simplification in dependent type theory}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {49--56}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577832}, doi = {10.1145/1577824.1577832}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/Reed09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/lfmtp/WestbrookSA09, author = {Edwin M. Westbrook and Aaron Stump and Evan Austin}, editor = {James Cheney and Amy P. Felty}, title = {The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings}, booktitle = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, pages = {74--83}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1577824.1577836}, doi = {10.1145/1577824.1577836}, timestamp = {Tue, 06 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/WestbrookSA09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2008, editor = {Andreas Abel and Christian Urban}, title = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, publisher = {Elsevier}, year = {2009}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/228/suppl/C}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2008.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2009, editor = {James Cheney and Amy P. Felty}, title = {Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, {LFMTP} '09, McGill University, Montreal, Canada, August 2, 2009}, publisher = {{ACM}}, year = {2009}, url = {http://dl.acm.org/citation.cfm?id=1577824}, isbn = {978-1-60558-529-1}, timestamp = {Mon, 12 Mar 2012 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2009.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/AbelU09, author = {Andreas Abel and Christian Urban}, editor = {Andreas Abel and Christian Urban}, title = {Preface}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {1}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.112}, doi = {10.1016/J.ENTCS.2008.12.112}, timestamp = {Fri, 24 Feb 2023 10:26:24 +0100}, biburl = {https://dblp.org/rec/journals/entcs/AbelU09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Baelde09, author = {David Baelde}, editor = {Andreas Abel and Christian Urban}, title = {On the Expressivity of Minimal Generic Quantification}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {3--19}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.113}, doi = {10.1016/J.ENTCS.2008.12.113}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Baelde09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Chapman09, author = {James Chapman}, editor = {Andreas Abel and Christian Urban}, title = {Type Theory Should Eat Itself}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {21--36}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.114}, doi = {10.1016/J.ENTCS.2008.12.114}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Chapman09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Cheney09, author = {James Cheney}, editor = {Andreas Abel and Christian Urban}, title = {A Simple Nominal Type Theory}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {37--52}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.115}, doi = {10.1016/J.ENTCS.2008.12.115}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Cheney09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Crary09, author = {Karl Crary}, editor = {Andreas Abel and Christian Urban}, title = {Explicit Contexts in {LF} (Extended Abstract)}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {53--68}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.116}, doi = {10.1016/J.ENTCS.2008.12.116}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Crary09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/DunfieldP09, author = {Jana Dunfield and Brigitte Pientka}, editor = {Andreas Abel and Christian Urban}, title = {Case Analysis of Higher-Order Data}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {69--84}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.117}, doi = {10.1016/J.ENTCS.2008.12.117}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/DunfieldP09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/GacekMN09, author = {Andrew Gacek and Dale Miller and Gopalan Nadathur}, editor = {Andreas Abel and Christian Urban}, title = {Reasoning in Abella about Structural Operational Semantics Specifications}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {85--100}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.118}, doi = {10.1016/J.ENTCS.2008.12.118}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/GacekMN09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Leivant09, author = {Daniel Leivant}, editor = {Andreas Abel and Christian Urban}, title = {Inductive Completeness of Logics of Programs}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {101--112}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.119}, doi = {10.1016/J.ENTCS.2008.12.119}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Leivant09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/PoswolskyS09, author = {Adam Poswolsky and Carsten Sch{\"{u}}rmann}, editor = {Andreas Abel and Christian Urban}, title = {System Description: Delphin - {A} Functional Programming Language for Deductive Systems}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {113--120}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.120}, doi = {10.1016/J.ENTCS.2008.12.120}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/PoswolskyS09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Stump09, author = {Aaron Stump}, editor = {Andreas Abel and Christian Urban}, title = {Proof Checking Technology for Satisfiability Modulo Theories}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {121--133}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.121}, doi = {10.1016/J.ENTCS.2008.12.121}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Stump09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Tiu09, author = {Alwen Tiu}, editor = {Andreas Abel and Christian Urban}, title = {On the Role of Names in Reasoning about lambda-tree Syntax Specifications}, booktitle = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008}, series = {Electronic Notes in Theoretical Computer Science}, volume = {228}, pages = {135--150}, publisher = {Elsevier}, year = {2008}, url = {https://doi.org/10.1016/j.entcs.2008.12.122}, doi = {10.1016/J.ENTCS.2008.12.122}, timestamp = {Fri, 24 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Tiu09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2007, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, publisher = {Elsevier}, year = {2008}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/196/suppl/C}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2007.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/BuisseD08, author = {Alexandre Buisse and Peter Dybjer}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Towards Formalizing Categorical Models of Type Theory in Type Theory}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {137--151}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.023}, doi = {10.1016/J.ENTCS.2007.09.023}, timestamp = {Thu, 09 Feb 2023 11:15:18 +0100}, biburl = {https://dblp.org/rec/journals/entcs/BuisseD08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Callaghan08, author = {Paul Callaghan}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Coercive Subtyping via Mappings of Reduction Behaviour}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {53--68}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.017}, doi = {10.1016/J.ENTCS.2007.09.017}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Callaghan08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/GabbayL08, author = {Murdoch Gabbay and St{\'{e}}phane Lengrand}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {The lambda-context Calculus}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {19--35}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.015}, doi = {10.1016/J.ENTCS.2007.09.015}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/GabbayL08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Lindblad08, author = {Fredrik Lindblad}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Higher-Order Proof Construction Based on First-Order Narrowing}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {69--84}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.018}, doi = {10.1016/J.ENTCS.2007.09.018}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Lindblad08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/LovasP08, author = {William Lovas and Frank Pfenning}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {A Bidirectional Refinement Type System for {LF}}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {113--128}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.021}, doi = {10.1016/J.ENTCS.2007.09.021}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/LovasP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/MomiglianoMF08, author = {Alberto Momigliano and Alan J. Martin and Amy P. Felty}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Two-Level Hybrid: {A} System for Reasoning Using Higher-Order Abstract Syntax}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {85--93}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.019}, doi = {10.1016/J.ENTCS.2007.09.019}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/MomiglianoMF08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/NarbouxU08, author = {Julien Narboux and Christian Urban}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {3--18}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.014}, doi = {10.1016/J.ENTCS.2007.09.014}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/NarbouxU08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/PientkaLP08, author = {Brigitte Pientka and Xi Li and Florent Pompigne}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Focusing the Inverse Method for {LF:} {A} Preliminary Report}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {95--112}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.020}, doi = {10.1016/J.ENTCS.2007.09.020}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/PientkaLP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/PientkaS08, author = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Preface}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {1}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.013}, doi = {10.1016/J.ENTCS.2007.09.013}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/PientkaS08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Schack-Nielsen08, author = {Anders Schack{-}Nielsen}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Induction on Concurrent Terms}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {37--51}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.016}, doi = {10.1016/J.ENTCS.2007.09.016}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Schack-Nielsen08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/ZellerSD08, author = {Michael Zeller and Aaron Stump and Morgan Deters}, editor = {Brigitte Pientka and Carsten Sch{\"{u}}rmann}, title = {Signature Compilation for the Edinburgh Logical Framework}, booktitle = {Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@CADE 2007, Bremen, Germany, July 15, 2007}, series = {Electronic Notes in Theoretical Computer Science}, volume = {196}, pages = {129--135}, publisher = {Elsevier}, year = {2007}, url = {https://doi.org/10.1016/j.entcs.2007.09.022}, doi = {10.1016/J.ENTCS.2007.09.022}, timestamp = {Thu, 09 Feb 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/ZellerSD08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/lfmtp/2006, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, publisher = {Elsevier}, year = {2007}, url = {https://www.sciencedirect.com/journal/electronic-notes-in-theoretical-computer-science/vol/174/issue/5}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/lfmtp/2006.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/AppelL07, author = {Andrew W. Appel and Xavier Leroy}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {95--108}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.020}, doi = {10.1016/J.ENTCS.2007.01.020}, timestamp = {Fri, 27 Jan 2023 13:31:48 +0100}, biburl = {https://dblp.org/rec/journals/entcs/AppelL07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/AydemirBW07, author = {Brian E. Aydemir and Aaron Bohannon and Stephanie Weirich}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Nominal Reasoning Techniques in Coq: (Extended Abstract)}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {69--77}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.028}, doi = {10.1016/J.ENTCS.2007.01.028}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/AydemirBW07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/BerghoferU07, author = {Stefan Berghofer and Christian Urban}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {A Head-to-Head Comparison of de Bruijn Indices and Names}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {53--67}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.018}, doi = {10.1016/J.ENTCS.2007.01.018}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/BerghoferU07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Brown07, author = {Chad E. Brown}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Encoding Functional Relations in Scunak}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {127--139}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.022}, doi = {10.1016/J.ENTCS.2007.01.022}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Brown07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/DonnellyX07, author = {Kevin Donnelly and Hongwei Xi}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System {F}}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {109--125}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.021}, doi = {10.1016/J.ENTCS.2007.01.021}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/DonnellyX07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Gabbay07, author = {Murdoch Gabbay}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Hierarchical Nominal Terms and Their Theory of Rewriting}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {37--52}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.017}, doi = {10.1016/J.ENTCS.2007.01.017}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Gabbay07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Hernest07, author = {Mircea{-}Dan Hernest}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Synthesis of Moduli of Uniform Continuity by the Monotone Dialectica Interpretation in the Proof-system MinLog}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {141--149}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.023}, doi = {10.1016/J.ENTCS.2007.01.023}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Hernest07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/HickeyNYK07, author = {Jason Hickey and Aleksey Nogin and Xin Yu and Alexei Kopylov}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Practical Reflection for Sequent Logics}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {79--94}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.019}, doi = {10.1016/J.ENTCS.2007.01.019}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/HickeyNYK07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/MomiglianoP07, author = {Alberto Momigliano and Brigitte Pientka}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Preface}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {1--2}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.015}, doi = {10.1016/J.ENTCS.2007.01.015}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/MomiglianoP07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Schopp07, author = {Ulrich Sch{\"{o}}pp}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {Modelling Generic Judgements}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {19--35}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.027}, doi = {10.1016/J.ENTCS.2007.01.027}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Schopp07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/entcs/Tiu07, author = {Alwen Tiu}, editor = {Alberto Momigliano and Brigitte Pientka}, title = {A Logic for Reasoning about Generic Judgments}, booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle, WA, USA, August 16, 2006}, series = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {5}, pages = {3--18}, publisher = {Elsevier}, year = {2006}, url = {https://doi.org/10.1016/j.entcs.2007.01.016}, doi = {10.1016/J.ENTCS.2007.01.016}, timestamp = {Fri, 27 Jan 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/entcs/Tiu07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.