Using Typed Lambda Calculus to Implement Formal Systems on a Machine

this paper and the LF. In particular the idea of having an operator T : Prop ! Type appears already in De Bruijn's earlier work, as does the idea of having several judgements. The paper [24] describes the basic features of the LF. In this paper we are going to provide a broader illustration of its applicability and discuss to what extent it is successful. The analysis (of the formal presentation) of a system carried out through encoding often illuminates the system itself. This paper will also deal with this phenomenon