Sign in
LFMTP
2009
2013
2017
2021
2009
2021
Keyphrases
Publications
2021
Gilles Dowek
Interacting Safely with an Unsafe Environment.
LFMTP
(2021)
Giselle Reis
Facilitating Meta-Theory Reasoning (Invited Paper).
LFMTP
(2021)
Mary Southern
,
Gopalan Nadathur
Adelfa: A System for Reasoning about LF Specifications.
LFMTP
(2021)
Johannes Schoisswohl
,
Laura Kovács
Automating Induction by Reflection.
LFMTP
(2021)
Florian Rabe
,
Navid Roux
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style.
LFMTP
(2021)
Matthieu Sozeau
Touring the MetaCoq Project (Invited Paper).
LFMTP
(2021)
Laila El-Beheiry
,
Giselle Reis
,
Ammar Karkour
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts.
LFMTP
(2021)
Qinxiang Cao
,
Xiwei Wu
Countability of Inductive Types Formalized in the Object-Logic Level.
LFMTP
(2021)
volume 337, 2021
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021.
LFMTP
337 (2021)
volume 332, 2021
Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020.
LFMTP
332 (2021)
2020
Bruno Barras
,
Valentin Maestracci
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory.
LFMTP
(2020)
Petros Papapanagiotou
,
Jacques D. Fleuriot
Object-Level Reasoning with Logics Encoded in HOL Light.
LFMTP
(2020)
Arve Gengelbach
,
Johannes Åman Pohjola
,
Tjark Weber
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.
LFMTP
(2020)
Tarmo Uustalu
,
Niccolò Veltri
,
Noam Zeilberger
Deductive Systems and Coherence for Skew Prounital Closed Categories.
LFMTP
(2020)
2016
Rohan Jacob-Rao
,
Andrew Cave
,
Brigitte Pientka
Mechanizing Proofs about Mendler-style Recursion.
LFMTP
(2016)
Joachim Breitner
The Incredible Proof Machine (Invited Talk).
LFMTP
(2016)
Chelsea Battell
,
Amy P. Felty
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid.
LFMTP
(2016)
Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016
LFMTP
(2016)
Cvetan Dunchev
,
Claudio Sacerdoti Coen
,
Enrico Tassi
Implementing HOL in an Higher Order Logic Programming Language.
LFMTP
(2016)
Raphaël Cauderlier
A Rewrite System for Proof Constructivization.
LFMTP
(2016)
2015
Amy P. Felty
,
Alberto Momigliano
,
Brigitte Pientka
An Open Challenge Problem Repository for Systems Supporting Binders.
LFMTP
(2015)
Roly Perera
,
James Cheney
Proof-relevant pi-calculus.
LFMTP
(2015)
Andrew Cave
,
Brigitte Pientka
A Case Study on Logical Relations using Contextual Types.
LFMTP
(2015)
Ronan Saillard
Rewriting Modulo βin the λΠ-Calculus Modulo.
LFMTP
(2015)
Furio Honsell
,
Luigi Liquori
,
Petar Maksimovic
,
Ivan Scagnetto
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks.
LFMTP
(2015)
Nicolas Guenot
,
Daniel Gustafsson
Sequent Calculus and Equational Programming.
LFMTP
(2015)
volume 185, 2015
Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015.
LFMTP
185 (2015)
2014
Jesper Bengtson
Session Types Meet Separation Logic.
LFMTP
(2014)
Olivier Savary Bélanger
,
Kaustuv Chaudhuri
Automatically Deriving Schematic Theorems for Dynamic Contexts.
LFMTP
(2014)
Abhishek Anand
,
Vincent Rahli
A Generic Approach to Proofs about Substitution.
LFMTP
(2014)
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, Vienna, Austria, July 17, 2014
LFMTP
(2014)
Alberto Ciaffaglione
,
Ivan Scagnetto
Internal Adequacy of Bookkeeping in Coq.
LFMTP
(2014)
Iliano Cervesato
Proof-Theoretic Foundations of Indexing in Logic Programming.
LFMTP
(2014)
Thorsten Altenkirch
,
Nuo Li
,
Ondrej Rypacek
Some constructions on ω-groupoids.
LFMTP
(2014)
Gopalan Nadathur
A Framework for the Verified Transformation of Functional Programs.
LFMTP
(2014)
Edwin C. Brady
Idris: Implementing a Dependently Typed Programming Language.
LFMTP
(2014)
Taus Brock-Nannestad
,
Nicolas Guenot
,
Agata Murawska
,
Carsten Schürmann
Hybrid Extensions in a Logical Framework.
LFMTP
(2014)
2013
Mahfuza Farooque
,
Stéphane Graham-Lengrand
,
Assia Mahboubi
) and a proof-search strategy for the focused sequent calculus.
LFMTP
(2013)
Andrew Cave
,
Brigitte Pientka
First-class substitutions in contextual type theory.
LFMTP
(2013)
Floris van Doorn
,
Herman Geuvers
,
Freek Wiedijk
Explicit convertibility proofs in pure type systems.
LFMTP
(2013)
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)
Yuting Wang
,
Gopalan Nadathur
Towards extracting explicit proofs from totality checking in twelf.
LFMTP
(2013)
Ulrik Terp Rasmussen
,
Andrzej Filinski
Structural logical relations with case analysis and equality reasoning.
LFMTP
(2013)
Dale Miller
Foundational proof certificates: making proof universal and permanent.
LFMTP
(2013)
Furio Honsell
25 years of formal proof cultures: some problems, some philosophy, bright future.
LFMTP
(2013)
2011
Ranald Clouston
Nominal Logic with Equations Only
LFMTP
(2011)
Maxime Beauquier
,
Carsten Schürmann
A Bigraph Relational Model
LFMTP
(2011)
Andreas Abel
,
Nicolai Kraus
A Lambda Term Representation Inspired by Linear Ordered Logic
LFMTP
(2011)
Alan J. Martin
,
Amy P. Felty
An Improved Implementation and Abstract Interface for Hybrid
LFMTP
(2011)
volume 71, 2011
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011.
LFMTP
71 (2011)