Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces

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 lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vec...

Full description

Bibliographic Details
Main Authors: B. Valiron, S. Zdancewic
Format: Article
Language:English
Published: Alexandru Ioan Cuza University of Iasi 2014-12-01
Series:Scientific Annals of Computer Science
Online Access:http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_5.pdf