Editing Logical framework (section)

==Further reading==
* {{cite book|editor=[[Helmut Schwichtenberg]], Ralf Steinbrüggen|title=Proof and system-reliability|chapter=Logical frameworks – a brief introduction|year=2002| publisher=[[Springer Science+Business Media|Springer]] |isbn=978-1-4020-0608-1|author=[[Frank Pfenning]]|url=https://www.cs.cmu.edu/~fp/papers/mdorf01.pdf}}
*[[Robert Harper (computer scientist)|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 <math>\lambda</math>-calculus''. Journal of Logic and Computation 12(6), 1061-1104, 2002.  
* Per Martin-Löf. "[https://web.archive.org/web/20060104064335/http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.html 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 [http://www.cs.chalmers.se/Cs/Research/Logic/book/ a free version] has been made available.)
*David Pym. ''A Note on the Proof Theory of the <math>\lambda\Pi</math>-calculus''. Studia Logica 54: 199-230, 1995. 
*David Pym and [[Lincoln Wallen]]. ''Proof-search in the <math>\lambda\Pi</math>-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 <math>\lambda\Pi</math>-calculus.'' International Journal of Foundations of Computer Science 3(3), 333-378, 1992.