Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Giselle Reis |
Facilitating Meta-Theory Reasoning (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 1-12, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Matthieu Sozeau |
Touring the MetaCoq Project (Invited Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 13-29, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Claudio Sacerdoti Coen, Alwen Tiu (eds.) |
Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Schoisswohl, Laura Kovács |
Automating Induction by Reflection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 39-54, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek |
Interacting Safely with an Unsafe Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 30-38, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Elaine Pimentel, Enrico Tassi (eds.) |
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Laila El-Beheiry, Giselle Reis, Ammar Karkour |
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 71-87, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Mary Southern, Gopalan Nadathur |
Adelfa: A System for Reasoning about LF Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 104-120, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Qinxiang Cao, Xiwei Wu |
Countability of Inductive Types Formalized in the Object-Logic Level. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 55-70, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Florian Rabe 0001, Navid Roux |
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021., pp. 88-103, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
1 | Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber |
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 1-17, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Petros Papapanagiotou, Jacques D. Fleuriot |
Object-Level Reasoning with Logics Encoded in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 18-34, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Barras, Valentin Maestracci |
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 54-67, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger |
Deductive Systems and Coherence for Skew Prounital Closed Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 35-53, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
1 | Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi |
Implementing HOL in an Higher Order Logic Programming Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 4:1-4:10, 2016, ACM, 978-1-4503-4777-8. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Raphaël Cauderlier |
A Rewrite System for Proof Constructivization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 2:1-2:7, 2016, ACM, 978-1-4503-4777-8. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Joachim Breitner |
The Incredible Proof Machine (Invited Talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 5:1, 2016, ACM, 978-1-4503-4777-8. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka |
Mechanizing Proofs about Mendler-style Recursion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 1:1-1:9, 2016, ACM, 978-1-4503-4777-8. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Chelsea Battell, Amy P. Felty |
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 3:1-3:10, 2016, ACM, 978-1-4503-4777-8. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek, Daniel R. Licata, Sandra Alves (eds.) |
Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016 ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![ACM, 978-1-4503-4777-8 The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto |
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 3-17, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Andrew Cave, Brigitte Pientka |
A Case Study on Logical Relations using Contextual Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 33-45, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Iliano Cervesato, Kaustuv Chaudhuri (eds.) |
Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Roly Perera, James Cheney |
Proof-relevant pi-calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 46-70, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Nicolas Guenot, Daniel Gustafsson |
Sequent Calculus and Equational Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 102-109, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Ronan Saillard |
Rewriting Modulo βin the λΠ-Calculus Modulo. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 87-101, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Alberto Momigliano, Brigitte Pientka |
An Open Challenge Problem Repository for Systems Supporting Binders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., pp. 18-32, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Iliano Cervesato |
Proof-Theoretic Foundations of Indexing in Logic Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 7: 1-7: 9, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Gopalan Nadathur |
A Framework for the Verified Transformation of Functional Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 3: 1, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Taus Brock-Nannestad, Nicolas Guenot, Agata Murawska, Carsten Schürmann 0001 |
Hybrid Extensions in a Logical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 6: 1-6: 8, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Jesper Bengtson |
Session Types Meet Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 1: 1, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Savary Bélanger, Kaustuv Chaudhuri |
Automatically Deriving Schematic Theorems for Dynamic Contexts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 9: 1-9: 8, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Abhishek Anand, Vincent Rahli |
A Generic Approach to Proofs about Substitution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 5: 1-5: 8, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Amy P. Felty, Brigitte Pientka (eds.) |
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014 ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![ACM, 978-1-4503-2817-3 The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Ciaffaglione, Ivan Scagnetto |
Internal Adequacy of Bookkeeping in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 8: 1-8: 8, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Thorsten Altenkirch, Nuo Li, Ondrej Rypacek |
Some constructions on ω-groupoids. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 4: 1-4: 8, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Edwin C. Brady |
Idris: Implementing a Dependently Typed Programming Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014, pp. 2: 1, 2014, ACM, 978-1-4503-2817-3. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
1 | Ulrik Terp Rasmussen, Andrzej Filinski |
Structural logical relations with case analysis and equality reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 43-54, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi |
A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 3-14, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Andrew Cave, Brigitte Pientka |
First-class substitutions in contextual type theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 15-24, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Momigliano, Brigitte Pientka, Randy Pollack (eds.) |
Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013 ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![ACM, 978-1-4503-2382-6 The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Dale Miller 0001 |
Foundational proof certificates: making proof universal and permanent. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 1-2, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Furio Honsell |
25 years of formal proof cultures: some problems, some philosophy, bright future. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 37-42, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Yuting Wang 0001, Gopalan Nadathur |
Towards extracting explicit proofs from totality checking in twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 55-66, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Floris van Doorn, Herman Geuvers, Freek Wiedijk |
Explicit convertibility proofs in pure type systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 25-36, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Ranald Clouston |
Nominal Logic with Equations Only ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 44-57, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001, Nicolai Kraus |
A Lambda Term Representation Inspired by Linear Ordered Logic ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 1-13, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Gopalan Nadathur (eds.) |
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Murdoch James Gabbay, Dominic P. Mulligan |
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 58-75, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Maxime Beauquier, Carsten Schürmann |
A Bigraph Relational Model ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 14-28, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Alan J. Martin, Amy P. Felty |
An Improved Implementation and Abstract Interface for Hybrid ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 76-90, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Mathieu Boespflug, Brigitte Pientka |
Multi-level Contextual Type Theory ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011., pp. 29-43, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Daniel R. Licata, Robert Harper 0001 |
A Monadic Formalization of ML5 ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 69-83, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Maribel Fernández, Murdoch James Gabbay |
Closed nominal rewriting and efficiently computable nominal algebra equality ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 37-51, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Anders Schack-Nielsen, Carsten Schürmann |
Pattern Unification for the Lambda Calculus with Linear and Affine Types ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 101-116, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk |
Pure Type Systems without Explicit Contexts ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 53-67, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | John Tang Boyland |
Generating Bijections between HOAS and the Natural Numbers ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 21-35, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Florian Rabe 0001 |
Representing Isabelle in LF ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 85-99, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Karl Crary, Marino Miculan (eds.) |
Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001, Brigitte Pientka |
Explicit Substitutions for Contextual Type Theory ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2010, Edinburgh, UK, 14th July 2010., pp. 5-20, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
1 | Florian Rabe 0001, Carsten Schürmann |
A practical module system for LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 40-48, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Karl Crary |
A syntactic account of singleton types via hereditary substitution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 21-29, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Douglas J. Howe |
Higher-order abstract syntax in classical higher-order logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 1-11, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu 0001 |
Theory support for weak higher order abstract syntax in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 12-20, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | James Cheney, Amy P. Felty (eds.) |
Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009 ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![ACM, 978-1-60558-529-1 The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP BibTeX RDF |
|
1 | Jason Reed 0001 |
Higher-order constraint simplification in dependent type theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 49-56, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Guillaume Burel, Gilles Dowek |
How can we prove that a proof search method is not an instance of another? ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 84-87, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Edwin M. Westbrook, Aaron Stump, Evan Austin |
The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 74-83, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Murdoch James Gabbay, Dominic P. Mulligan |
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 64-73, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Robin Adams 0001 |
Coercive subtyping in lambda-free logical frameworks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 30-39, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal, Jan Schwinghammer |
Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '09, McGill University, Montreal, Canada, August 2, 2009, pp. 57-63, 2009, ACM, 978-1-60558-529-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|