  Finally, we mention that in the area of encoding computation as proof normalization, linear logic has been used to provide a type-based description of polytime recursive functions. For example, M.  Hofmann  (2003)  introduced a \(\lambda\)-calculus with modal and linear types that extended the function algebra of  Bellantoni &amp; Cook 1992  to higher types. Types based on linear logic have also been used within functional programs: see  Guzman &amp; Hudak 1990  and  Wadler 1991.