Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
88 | Frank Pfenning, Carsten Schürmann |
System Description: Twelf - A Meta-Logical Framework for Deductive Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 202-206, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
70 | Carsten Schürmann 0001, Jeffrey Sarnat |
Structural Logical Relations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pp. 69-80, 2008, IEEE Computer Society, 978-0-7695-3183-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pp. 187-198, 2010, ACM, 978-1-4503-0132-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 9(3), pp. 16:1-16:26, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, pp. 150-166, 2006, Springer, 3-540-48281-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Carsten Schürmann |
Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings, pp. 22-23, 2004, Springer, 3-540-21402-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
51 | Daniel K. Lee, Karl Crary, Robert Harper 0001 |
Towards a mechanized metatheory of standard ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pp. 173-184, 2007, ACM, 1-59593-575-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, 21st International Conference, ICLP 2005, Sitges, Spain, October 2-5, 2005, Proceedings, pp. 387-401, 2005, Springer, 3-540-29208-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
37 | Brigitte Pientka, Frank Pfenning |
Optimizing Higher-Order Pattern Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 473-487, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
37 | Neophytos G. Michael, Andrew W. Appel |
Machine Instruction Syntax and Semantics in Higher Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 7-24, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
37 | Carsten Schürmann, Frank Pfenning |
Automated Theorem Proving in a Simple Meta-Logic for LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 286-300, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
33 | Mary Southern, Gopalan Nadathur |
A Lambda Prolog Based Animation of Twelf Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1407.1545, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP BibTeX RDF |
|
33 | Yuting Wang 0001, Gopalan Nadathur |
Towards Extracting Explicit Proofs from Totality Checking in Twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1307.1738, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
33 | Yuting Wang 0001, Gopalan Nadathur |
Towards extracting explicit proofs from totality checking in twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, Boston, Massachusetts, USA, September 23, 2013, pp. 55-66, 2013, ACM, 978-1-4503-2382-6. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
33 | Carsten Schürmann 0001 |
The Twelf Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 79-83, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
33 | Andreas Abel 0001 |
Normalization for the Simply-Typed Lambda-Calculus in Twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFM@IJCAR ![In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, LFM@IJCAR 2004. Cork, Ireland, July 5, 2004, pp. 3-16, 2004, Elsevier. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Andrew W. Appel, Amy P. Felty |
Polymorphic lemmas and definitions in Lambda Prolog and Twelf ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/0403010, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
33 | Andrew W. Appel, Amy P. Felty |
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theory Pract. Log. Program. ![In: Theory Pract. Log. Program. 4(1-2), pp. 1-39, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Jeremy E. Dawson, Rajeev Goré |
Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CATS ![In: Computing: The Australasian Theory Symposium, CATS 2001, Gold Coast, Australia, January 29-30, 2001, pp. 89-103, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
18 | Jeffrey Sarnat, Carsten Schürmann 0001 |
Lexicographic Path Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, pp. 279-293, 2009, Springer, 978-3-642-02272-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
18 | Daniel Marino, Todd D. Millstein |
A generic type-and-effect system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pp. 39-50, 2009, ACM, 978-1-60558-420-1. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
type-and-effect systems |
18 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the Metatheory of LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pp. 45-56, 2008, IEEE Computer Society, 978-0-7695-3183-0. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 320-326, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
18 | Brigitte Pientka |
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 246-261, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
18 | Umut A. Acar, Matthias Blume, Jacob Donham |
A Consistent Semantics of Self-adjusting Computation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, pp. 458-474, 2007, Springer, 978-3-540-71314-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pp. 1-12, 2007, ACM, 978-1-59593-815-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
18 | Brigitte Pientka |
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 362-376, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
18 | Brigitte Pientka |
Verifying Termination and Reduction Properties about Higher-Order Logic Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 34(2), pp. 179-207, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
termination, Logical frameworks |
18 | Gopalan Nadathur, Natalie Linnell |
Practical Higher-Order Pattern Unification with On-the-Fly Raising. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, 21st International Conference, ICLP 2005, Sitges, Spain, October 2-5, 2005, Proceedings, pp. 371-386, 2005, Springer, 3-540-29208-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
18 | Robert Harper 0001 |
Mechanizing the meta-theory of programming languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pp. 240, 2005, ACM, 1-59593-064-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
18 | Penny Anderson, Frank Pfenning |
Verifying Uniqueness in a Logical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 18-33, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
18 | Alberto Momigliano, Simon Ambler |
Multi-level Meta-reasoning with Higher-Order Abstract Syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pp. 375-391, 2003, Springer, 3-540-00897-7. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
18 | Brigitte Pientka |
Higher-Order Substitution Tree Indexing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, 19th International Conference, ICLP 2003, Mumbai, India, December 9-13, 2003, Proceedings, pp. 377-391, 2003, Springer, 3-540-20642-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
18 | Karl Crary, Susmit Sarkar |
Foundational Certified Code in a Metalogical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 106-120, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pp. 75-, 2002, IEEE Computer Society, 0-7695-1483-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
18 | Brigitte Pientka |
Termination and Reduction Checking for Higher-Order Logic Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 401-415, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|