Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

Benoît Valiron, Steve Zdancewic

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like la…