Les preuves et les programmes peuvent être considérés comme étant structurés par plusieurs opérations : a minima une opération de composition (d’une preuve de $A$ et de $A \Rightarrow B$, on peut déduire une preuve de $B$) et une opération de réduction (un programme se réduit en son résultat).
Nous étudions des langages permettant de représenter ces opérations pour des constructions logiques et calculatoires de plus en plus expressives.