@inproceedings{pfenning_system_1999,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {System {Description}: {Twelf} — {A} {Meta}-{Logical} {Framework} for {Deductive} {Systems}},
	isbn = {978-3-540-48660-2},
	shorttitle = {System {Description}},
	doi = {10/d3h8pw},
	abstract = {Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and the judgments-as-types methodology for specification [HHP93], a constraint logic programming interpreter for implementation [Pfe91], and the meta-logic M2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94].Twelf is written in Standard ML and runs under SML of New Jersey and MLWorks on Unix and Window platforms. The current version (1.2) is distributed with a complete manual, example suites, a tutorial in the form of on-line lecture notes [Pfe], and an Emacs interface. Source and binary distributions are accessible via the Twelf home page http://www.cs.cmu.edu/{\textasciitilde}twelf.},
	language = {en},
	booktitle = {Automated {Deduction} — {CADE}-16},
	publisher = {Springer},
	author = {Pfenning, Frank and Schürmann, Carsten},
	editor = {Ganzinger, Harald},
	year = {1999},
	note = {ZSCC: NoCitationData[s0]},
	keywords = {Deductive System, Logic Program, Logic Programming, Object Language, Operational Semantic},
	pages = {202--206}
}

{"_id":"3vquX2C7ycLd5PuYe","bibbaseid":"pfenning-schrmann-systemdescriptiontwelfametalogicalframeworkfordeductivesystems-1999","authorIDs":[],"author_short":["Pfenning, F.","Schürmann, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Berlin, Heidelberg","series":"Lecture Notes in Computer Science","title":"System Description: Twelf — A Meta-Logical Framework for Deductive Systems","isbn":"978-3-540-48660-2","shorttitle":"System Description","doi":"10/d3h8pw","abstract":"Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and the judgments-as-types methodology for specification [HHP93], a constraint logic programming interpreter for implementation [Pfe91], and the meta-logic M2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94].Twelf is written in Standard ML and runs under SML of New Jersey and MLWorks on Unix and Window platforms. The current version (1.2) is distributed with a complete manual, example suites, a tutorial in the form of on-line lecture notes [Pfe], and an Emacs interface. Source and binary distributions are accessible via the Twelf home page http://www.cs.cmu.edu/\\textasciitildetwelf.","language":"en","booktitle":"Automated Deduction — CADE-16","publisher":"Springer","author":[{"propositions":[],"lastnames":["Pfenning"],"firstnames":["Frank"],"suffixes":[]},{"propositions":[],"lastnames":["Schürmann"],"firstnames":["Carsten"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Ganzinger"],"firstnames":["Harald"],"suffixes":[]}],"year":"1999","note":"ZSCC: NoCitationData[s0]","keywords":"Deductive System, Logic Program, Logic Programming, Object Language, Operational Semantic","pages":"202–206","bibtex":"@inproceedings{pfenning_system_1999,\n\taddress = {Berlin, Heidelberg},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {System {Description}: {Twelf} — {A} {Meta}-{Logical} {Framework} for {Deductive} {Systems}},\n\tisbn = {978-3-540-48660-2},\n\tshorttitle = {System {Description}},\n\tdoi = {10/d3h8pw},\n\tabstract = {Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and the judgments-as-types methodology for specification [HHP93], a constraint logic programming interpreter for implementation [Pfe91], and the meta-logic M2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94].Twelf is written in Standard ML and runs under SML of New Jersey and MLWorks on Unix and Window platforms. The current version (1.2) is distributed with a complete manual, example suites, a tutorial in the form of on-line lecture notes [Pfe], and an Emacs interface. Source and binary distributions are accessible via the Twelf home page http://www.cs.cmu.edu/{\\textasciitilde}twelf.},\n\tlanguage = {en},\n\tbooktitle = {Automated {Deduction} — {CADE}-16},\n\tpublisher = {Springer},\n\tauthor = {Pfenning, Frank and Schürmann, Carsten},\n\teditor = {Ganzinger, Harald},\n\tyear = {1999},\n\tnote = {ZSCC: NoCitationData[s0]},\n\tkeywords = {Deductive System, Logic Program, Logic Programming, Object Language, Operational Semantic},\n\tpages = {202--206}\n}\n\n","author_short":["Pfenning, F.","Schürmann, C."],"editor_short":["Ganzinger, H."],"key":"pfenning_system_1999","id":"pfenning_system_1999","bibbaseid":"pfenning-schrmann-systemdescriptiontwelfametalogicalframeworkfordeductivesystems-1999","role":"author","urls":{},"keyword":["Deductive System","Logic Program","Logic Programming","Object Language","Operational Semantic"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:10.988Z","downloads":0,"keywords":["deductive system","logic program","logic programming","object language","operational semantic"],"search_terms":["system","description","twelf","meta","logical","framework","deductive","systems","pfenning","schürmann"],"title":"System Description: Twelf — A Meta-Logical Framework for Deductive Systems","year":1999,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}