| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Giselle Reis |
Facilitating Meta-Theory Reasoning (Invited Paper).  |
LFMTP  |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthieu Sozeau |
Touring the MetaCoq Project (Invited Paper). |
LFMTP |
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. |
LFMTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Schoisswohl, Laura Kovács |
Automating Induction by Reflection. |
LFMTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Dowek |
Interacting Safely with an Unsafe Environment. |
LFMTP |
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. |
LFMTP |
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. |
LFMTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Mary Southern, Gopalan Nadathur |
Adelfa: A System for Reasoning about LF Specifications. |
LFMTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Qinxiang Cao, Xiwei Wu |
Countability of Inductive Types Formalized in the Object-Logic Level. |
LFMTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Rabe 0001, Navid Roux |
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. |
LFMTP |
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. |
LFMTP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Petros Papapanagiotou, Jacques D. Fleuriot |
Object-Level Reasoning with Logics Encoded in HOL Light. |
LFMTP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Barras, Valentin Maestracci |
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. |
LFMTP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger |
Deductive Systems and Coherence for Skew Prounital Closed Categories. |
LFMTP |
2020 |
DBLP DOI BibTeX RDF |
|
| 1 | Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi |
Implementing HOL in an Higher Order Logic Programming Language. |
LFMTP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Raphaël Cauderlier |
A Rewrite System for Proof Constructivization. |
LFMTP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Joachim Breitner |
The Incredible Proof Machine (Invited Talk). |
LFMTP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Rohan Jacob-Rao, Andrew Cave, Brigitte Pientka |
Mechanizing Proofs about Mendler-style Recursion. |
LFMTP |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Chelsea Battell, Amy P. Felty |
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid. |
LFMTP |
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 |
LFMTP |
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. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Cave, Brigitte Pientka |
A Case Study on Logical Relations using Contextual Types. |
LFMTP |
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. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Roly Perera, James Cheney |
Proof-relevant pi-calculus. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Guenot, Daniel Gustafsson |
Sequent Calculus and Equational Programming. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ronan Saillard |
Rewriting Modulo βin the λΠ-Calculus Modulo. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Alberto Momigliano, Brigitte Pientka |
An Open Challenge Problem Repository for Systems Supporting Binders. |
LFMTP |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Iliano Cervesato |
Proof-Theoretic Foundations of Indexing in Logic Programming. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Gopalan Nadathur |
A Framework for the Verified Transformation of Functional Programs. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Taus Brock-Nannestad, Nicolas Guenot, Agata Murawska, Carsten Schürmann 0001 |
Hybrid Extensions in a Logical Framework. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Bengtson |
Session Types Meet Separation Logic. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Olivier Savary Bélanger, Kaustuv Chaudhuri |
Automatically Deriving Schematic Theorems for Dynamic Contexts. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Abhishek Anand, Vincent Rahli |
A Generic Approach to Proofs about Substitution. |
LFMTP |
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 |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Ciaffaglione, Ivan Scagnetto |
Internal Adequacy of Bookkeeping in Coq. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch, Nuo Li, Ondrej Rypacek |
Some constructions on ω-groupoids. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Edwin C. Brady |
Idris: Implementing a Dependently Typed Programming Language. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrik Terp Rasmussen, Andrzej Filinski |
Structural logical relations with case analysis and equality reasoning. |
LFMTP |
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. |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Cave, Brigitte Pientka |
First-class substitutions in contextual type theory. |
LFMTP |
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 |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Dale Miller 0001 |
Foundational proof certificates: making proof universal and permanent. |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Furio Honsell |
25 years of formal proof cultures: some problems, some philosophy, bright future. |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuting Wang 0001, Gopalan Nadathur |
Towards extracting explicit proofs from totality checking in twelf. |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Floris van Doorn, Herman Geuvers, Freek Wiedijk |
Explicit convertibility proofs in pure type systems. |
LFMTP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranald Clouston |
Nominal Logic with Equations Only |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel 0001, Nicolai Kraus |
A Lambda Term Representation Inspired by Linear Ordered Logic |
LFMTP |
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. |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Murdoch James Gabbay, Dominic P. Mulligan |
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Maxime Beauquier, Carsten Schürmann |
A Bigraph Relational Model |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan J. Martin, Amy P. Felty |
An Improved Implementation and Abstract Interface for Hybrid |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathieu Boespflug, Brigitte Pientka |
Multi-level Contextual Type Theory |
LFMTP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel R. Licata, Robert Harper 0001 |
A Monadic Formalization of ML5 |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Maribel Fernández, Murdoch James Gabbay |
Closed nominal rewriting and efficiently computable nominal algebra equality |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Anders Schack-Nielsen, Carsten Schürmann |
Pattern Unification for the Lambda Calculus with Linear and Affine Types |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk |
Pure Type Systems without Explicit Contexts |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | John Tang Boyland |
Generating Bijections between HOAS and the Natural Numbers |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Rabe 0001 |
Representing Isabelle in LF |
LFMTP |
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. |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel 0001, Brigitte Pientka |
Explicit Substitutions for Contextual Type Theory |
LFMTP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Rabe 0001, Carsten Schürmann |
A practical module system for LF. |
LFMTP |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Karl Crary |
A syntactic account of singleton types via hereditary substitution. |
LFMTP |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Douglas J. Howe |
Higher-order abstract syntax in classical higher-order logic. |
LFMTP |
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. |
LFMTP |
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 |
LFMTP |
2009 |
DBLP BibTeX RDF |
|
| 1 | Jason Reed 0001 |
Higher-order constraint simplification in dependent type theory. |
LFMTP |
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? |
LFMTP |
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. |
LFMTP |
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. |
LFMTP |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Robin Adams 0001 |
Coercive subtyping in lambda-free logical frameworks. |
LFMTP |
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. |
LFMTP |
2009 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license