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.
Type de document :
Rapport
[Intern report] A01-R-262 || bonfante01c, 2001, 13 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00100697
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:49:44
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100697, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

136