default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp
Full-text search
- > Home
Please enter a search query
- case-insensitive prefix search: default
e.g., sig matches "SIGIR" as well as "signal" - exact word search: append dollar sign ($) to word
e.g., graph$ matches "graph", but not "graphics" - boolean and: separate words by space
e.g., codd model - boolean or: connect words by pipe symbol (|)
e.g., graph|network
Update May 7, 2017: Please note that we had to disable the phrase search operator (.) and the boolean not operator (-) due to technical problems. For the time being, phrase search queries will yield regular prefix search result, and search terms preceded by a minus will be interpreted as regular (positive) search terms.
Author search results
no matches
Venue search results
no matches
Refine list
refine by author
- no options
- temporarily not available
refine by venue
- no options
- temporarily not available
refine by type
- no options
- temporarily not available
refine by access
- no options
- temporarily not available
refine by year
- no options
- temporarily not available
Publication search results
found 128 matches
- 2024
- Gabriele Cecilia, Alberto Momigliano:
A Beluga Formalization of the Harmony Lemma in the π-Calculus. LFMTP@FSCD 2024: 1-17 - Terrance Gray, Gopalan Nadathur:
Binding Contexts as Partitionable Multisets in Abella. LFMTP@FSCD 2024: 19-34 - Thomas Traversié:
Kuroda's Translation for the λπ-Calculus Modulo Theory and Dedukti. LFMTP@FSCD 2024: 35-48 - Thomas Traversié:
Proofs for Free in the λπ-Calculus Modulo Theory. LFMTP@FSCD 2024: 49-63 - Florian Rabe, Claudio Sacerdoti Coen:
Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024. EPTCS 404, 2024 [contents] - 2023
- Johanna Schwartzentruber, Brigitte Pientka:
Semi-Automation of Meta-Theoretic Proofs in Beluga. LFMTP@FSCD 2023: 20-35 - James T. Oswald
, Brandon Rozek:
Parallel Verification of Natural Deduction Proof Graphs. LFMTP@FSCD 2023: 36-51 - Antoine Gaulin, Brigitte Pientka:
Contextual Refinement Types. LFMTP@FSCD 2023: 4-19 - Félix Castro:
An Interpretation of E-HAw inside HAw. LFMTP@FSCD 2023: 52-66 - Alberto Ciaffaglione, Carlos Olarte:
Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2023, Rome, Italy, 2nd July 2023. EPTCS 396, 2023 [contents] - 2021
- Giselle Reis:
Facilitating Meta-Theory Reasoning (Invited Paper). LFMTP 2021: 1-12 - Gilles Dowek:
Interacting Safely with an Unsafe Environment. LFMTP 2021: 30-38 - Qinxiang Cao, Xiwei Wu:
Countability of Inductive Types Formalized in the Object-Logic Level. LFMTP 2021: 55-70 - Laila El-Beheiry, Giselle Reis, Ammar Karkour:
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts. LFMTP 2021: 71-87 - Florian Rabe, Navid Roux:
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style. LFMTP 2021: 88-103 - Mary Southern, Gopalan Nadathur:
Adelfa: A System for Reasoning about LF Specifications. LFMTP 2021: 104-120 - Johannes Schoisswohl, Laura Kovács:
Automating Induction by Reflection. LFMTP 2021: 39-54 - Matthieu Sozeau:
Touring the MetaCoq Project (Invited Paper). LFMTP 2021: 13-29 - Claudio Sacerdoti Coen, Alwen Tiu:
Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020. EPTCS 332, 2021 [contents] - Elaine Pimentel, Enrico Tassi:
Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2021, Pittsburgh, USA, 16th July 2021. EPTCS 337, 2021 [contents] - 2020
- Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber:
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. LFMTP 2020: 1-17 - Petros Papapanagiotou, Jacques D. Fleuriot:
Object-Level Reasoning with Logics Encoded in HOL Light. LFMTP 2020: 18-34 - Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger:
Deductive Systems and Coherence for Skew Prounital Closed Categories. LFMTP 2020: 35-53 - Bruno Barras, Valentin Maestracci:
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. LFMTP 2020: 54-67 - 2019
- Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa:
A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. LFMTP@LICS 2019: 8-23 - Michael Kohlhase, Jan Frederik Schaefer:
GF + MMT = GLF - From Language to Semantics through LF. LFMTP@LICS 2019: 24-39 - Dennis Müller, Florian Rabe:
Rapid Prototyping Formal Systems in MMT: 5 Case Studies. LFMTP@LICS 2019: 40-54 - Aaron Stump:
A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille. LFMTP@LICS 2019: 55-67 - Dale Miller, Ivan Scagnetto:
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019. EPTCS 307, 2019 [contents] - 2018
- Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling:
The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD 2018: 1-10
skipping 98 more matches
loading more results 
failed to load more results, please try again later
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.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
retrieved on 2024-12-21 11:00 CET 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:
