Carnegie Mellon University. Twelf includes a logic programming engine meta-theoretic reasoning about logic programs (termination, coverage, etc.) an inductive meta-logical theorem prover See also Grammatical Framework Turnstile (symbol) References Further reading Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993. Arnon Avron, Furio Honsell, Ian Mason and Randy Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309-354, 1992. Robert Harper. An Equational Formulation of LF. Technical Report, University of Edinburgh, 1988. LFCS report ECS-LFCS-88-67. Robert Harper, Donald Sannella and Andrzej Tarlecki. Structured Theory Presentations and Logic Representations. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994. Samin Ishtiaq and David Pym. A Relevant Analysis of Natural Deduction. Journal of Logic and Computation 8, 809-838, 1998. Samin Ishtiaq and David Pym. Kripke Resource Models of a Dependently-typed, Bunched -calculus. Journal of Logic and Computation 12(6), 1061-1104, 2002. Per Martin-Löf. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws." "Nordic Journal of Philosophical Logic", 1(1): 11-60, 1996. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.) David Pym. A Note on the Proof Theory of the -calculus. Studia Logica 54: 199-230, 1995. David Pym and Lincoln Wallen. Proof-search in the -calculus. In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991. Didier Galmiche and David Pym. Proof-search in type-theoretic languages:an introduction. Theoretical Computer Science 232 (2000) 5-53. Philippa Gardner. Representing Logics in Type Theory. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227. Gilles Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of Lecture Notes in Computer Science, 139-145, 1993. David Pym. Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990. David Pym. A Unification Algorithm for the -calculus. International Journal of Foundations of Computer Science 3(3), 333-378, 1992. External links Specific Logical Frameworks and Implementations (a list maintained by Frank Pfenning, but mostly dead links from 1997) Logic in computer science Type theory Proof assistants Dependently typed programming