The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Searching for twelf with no syntactic query expansion in all metadata.

Publication years (Num. hits)
1998-2004 (15) 2005-2009 (17) 2010-2014 (4)
Publication types (Num. hits)
article(6) inproceedings(30)
Venues (Conferences, Journals, ...)
CADE(5) CoRR(3) ICLP(3) IJCAR(3) LICS(3) TPHOLs(3) ICFP(2) ACM Trans. Comput. Log.(1) CATS(1) ESOP(1) FLOPS(1) FoSSaCS(1) J. Autom. Reason.(1) LFM@IJCAR(1) LFMTP(1) LPAR(1) More (+10 of total 21)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
The graphs summarize 15 occurrences of 11 keywords

Results
Found 36 publication records. Showing 36 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
88Frank Pfenning, Carsten Schürmann System Description: Twelf - A Meta-Logical Framework for Deductive Systems. Search on Bibsonomy CADE The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
70Carsten Schürmann 0001, Jeffrey Sarnat Structural Logical Relations. Search on Bibsonomy LICS The full citation details ... 2008 DBLP  DOI  BibTeX  RDF Twelf, Normalization, Logical Frameworks, Cut-Elimination, Logical Relations
55Zachary Snow, David Baelde, Gopalan Nadathur A meta-programming approach to realizing dependently typed logic programming. Search on Bibsonomy PPDP The full citation details ... 2010 DBLP  DOI  BibTeX  RDF dependently typed lambda calculi, higher-order logic programming, translation, logical frameworks
51Karl Crary, Susmit Sarkar Foundational certified code in the Twelf metalogical framework. Search on Bibsonomy ACM Trans. Comput. Log. The full citation details ... 2008 DBLP  DOI  BibTeX  RDF Foundational certified code, metalogic, logic programming
51Carsten Schürmann, Mark-Oliver Stehr An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. Search on Bibsonomy LPAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
51Carsten Schürmann Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework. Search on Bibsonomy FLOPS The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
51Daniel K. Lee, Karl Crary, Robert Harper 0001 Towards a mechanized metatheory of standard ML. Search on Bibsonomy POPL The full citation details ... 2007 DBLP  DOI  BibTeX  RDF language definitions, mechanized metatheory, twelf, standard ML, logical frameworks, type safety
37Susmit Sarkar, Brigitte Pientka, Karl Crary Small Proof Witnesses for LF. Search on Bibsonomy ICLP The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
37Brigitte Pientka, Frank Pfenning Optimizing Higher-Order Pattern Unification. Search on Bibsonomy CADE The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
37Neophytos G. Michael, Andrew W. Appel Machine Instruction Syntax and Semantics in Higher Order Logic. Search on Bibsonomy CADE The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
37Carsten Schürmann, Frank Pfenning Automated Theorem Proving in a Simple Meta-Logic for LF. Search on Bibsonomy CADE The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
33Mary Southern, Gopalan Nadathur A Lambda Prolog Based Animation of Twelf Specifications. Search on Bibsonomy CoRR The full citation details ... 2014 DBLP  BibTeX  RDF
33Yuting Wang 0001, Gopalan Nadathur Towards Extracting Explicit Proofs from Totality Checking in Twelf. Search on Bibsonomy CoRR The full citation details ... 2013 DBLP  BibTeX  RDF
33Yuting Wang 0001, Gopalan Nadathur Towards extracting explicit proofs from totality checking in twelf. Search on Bibsonomy LFMTP The full citation details ... 2013 DBLP  DOI  BibTeX  RDF
33Carsten Schürmann 0001 The Twelf Proof Assistant. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
33Andreas Abel 0001 Normalization for the Simply-Typed Lambda-Calculus in Twelf. Search on Bibsonomy LFM@IJCAR The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
33Andrew W. Appel, Amy P. Felty Polymorphic lemmas and definitions in Lambda Prolog and Twelf Search on Bibsonomy CoRR The full citation details ... 2004 DBLP  BibTeX  RDF
33Andrew W. Appel, Amy P. Felty Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. Search on Bibsonomy Theory Pract. Log. Program. The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
33Jeremy E. Dawson, Rajeev Goré Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle. Search on Bibsonomy CATS The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
18Jeffrey Sarnat, Carsten Schürmann 0001 Lexicographic Path Induction. Search on Bibsonomy TLCA The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
18Daniel Marino, Todd D. Millstein A generic type-and-effect system. Search on Bibsonomy TLDI The full citation details ... 2009 DBLP  DOI  BibTeX  RDF type-and-effect systems
18Christian Urban, James Cheney, Stefan Berghofer Mechanizing the Metatheory of LF. Search on Bibsonomy LICS The full citation details ... 2008 DBLP  DOI  BibTeX  RDF mechanized metatheory, logical frameworks, nominal logic
18Anders Schack-Nielsen, Carsten Schürmann Celf - A Logical Framework for Deductive and Concurrent Systems (System Description). Search on Bibsonomy IJCAR The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
18Brigitte Pientka Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
18Umut A. Acar, Matthias Blume, Jacob Donham A Consistent Semantics of Self-adjusting Computation. Search on Bibsonomy ESOP The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
18Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa Ott: effective tool support for the working semanticist. Search on Bibsonomy ICFP The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
18Brigitte Pientka Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. Search on Bibsonomy IJCAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
18Brigitte Pientka Verifying Termination and Reduction Properties about Higher-Order Logic Programs. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2005 DBLP  DOI  BibTeX  RDF termination, Logical frameworks
18Gopalan Nadathur, Natalie Linnell Practical Higher-Order Pattern Unification with On-the-Fly Raising. Search on Bibsonomy ICLP The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
18Robert Harper 0001 Mechanizing the meta-theory of programming languages. Search on Bibsonomy ICFP The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
18Penny Anderson, Frank Pfenning Verifying Uniqueness in a Logical Framework. Search on Bibsonomy TPHOLs The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
18Alberto Momigliano, Simon Ambler Multi-level Meta-reasoning with Higher-Order Abstract Syntax. Search on Bibsonomy FoSSaCS The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
18Brigitte Pientka Higher-Order Substitution Tree Indexing. Search on Bibsonomy ICLP The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
18Karl Crary, Susmit Sarkar Foundational Certified Code in a Metalogical Framework. Search on Bibsonomy CADE The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
18Amal J. Ahmed 0001, Andrew W. Appel, Roberto Virga A Stratified Semantics of General References A Stratified Semantics of General References. Search on Bibsonomy LICS The full citation details ... 2002 DBLP  DOI  BibTeX  RDF
18Brigitte Pientka Termination and Reduction Checking for Higher-Order Logic Programs. Search on Bibsonomy IJCAR The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #36 of 36 (100 per page; Change: )
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by L3S.
Previously maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license