HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A model of a dependent linear calculus

Guillaume Bonfante 1 François Lamarche 1 Thomas Streicher
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a full categorical account, based on Grothendieck fibrations, of what it means for a linear calculus to have dependent types, and we give a term assignment system which merges well with this axiomatization. We construct a model that obeys these categorical axioms, based on the category of graphs.
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:49:44 PM
Last modification on : Friday, February 4, 2022 - 3:34:49 AM


  • HAL Id : inria-00100697, version 1



Guillaume Bonfante, François Lamarche, Thomas Streicher. A model of a dependent linear calculus. [Intern report] A01-R-262 || bonfante01c, 2001, 13 p. ⟨inria-00100697⟩



Record views