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