Search results for "Twelf"

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