Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "stream:streams/conf/lfmtp:"
download as .bib file
@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 = {Fri, 22 Dec 2023 00:00:00 +0100},
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 = {Wed, 12 Sep 2018 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}
}
a service of 
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.
retrieved on 2024-05-11 07:46 CEST from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
