Coquand, Thierry, 1961-....
Coquand, Thierry
Thierry Coquand
VIAF ID: 117236995 ( Personal )
Permalink: http://viaf.org/viaf/117236995
Preferred Forms
-
-
- 100 1 _ ‡a Coquand, Thierry (sparse)
-
- 100 1 _ ‡a Coquand, Thierry
-
- 100 1 _ ‡a Coquand, Thierry ‡d 1961-
-
-
- 100 1 _ ‡a Coquand, Thierry, ‡d 1961-
- 100 1 _ ‡a Coquand, Thierry, ‡d 1961-....
- 100 0 _ ‡a Thierry Coquand
4xx's: Alternate Name Forms (9)
5xx's: Related Names (6)
- 510 2 _ ‡a Institutionen för Data- och Informationsteknik ‡e Affiliation
- 510 2 _ ‡a Institutionen för Data- och Informationsteknik
- 510 2 _ ‡a International Workshop TYPES'99 (12-06-1999 - 16-06-1999 : Lökeberg, Sweden)
- 510 2 _ ‡a TYPES '99 (1999 : Lökeberg, Sweden)
- 510 2 _ ‡a U.F.R. de Mathématiques
- 510 2 _ ‡a math : PARIS 7
Works
Title | Sources |
---|---|
Catégories faibles et structures supérieures afférentes en théorie des types. | |
Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting | |
Etendre la théorie des types à l'aide de modèles syntaxiques. | |
Étude formelle d'algorithmes efficaces en algèbre linéaire | |
Extending type theory with syntactic models | |
Formal study of efficient algorithms in linear algebra. | |
Homotopy type theory : univalent foundations of mathematics | |
Une investigation logique des systèmes d'interaction | |
Logical frameworks and meta-languages : actes = proceedings of the 2nd Workshop on ..., Santa Barbara, California, USA, June 25, 2000 | |
Mathematics, algorithms, proofs 05021 summary ; 09.01. - 14.01.05 | |
Modèles de l'univalence dans le cadre équivariant | |
Modules in type theory with generative definitions | |
nilregular element property | |
On Forcing and Classical Realizability | |
On lifting univalence to the equivariant setting. | |
On the formalization of foundations of geometry | |
Profondeur, dimension et résolutions en algèbre commutative : quelques aspects effectifs | |
Réalisabilité et paramétricité dans les systèmes de types purs | |
Semantics and implementation of an extension of ML for proving programs. | |
Sémantique et implantation d'une extension de ML pour la preuve de programmes | |
SEQUENTS QU'ON CALCULE : DE L'INTERPRETATION DU CALCUL DES SEQUENTS COMME CALCUL DE LAMBDA-TERMES ET COMME CALCUL DE STRATEGIES GAGNANTES | |
Sur la formalisation des fondements de la géométrie. | |
Sur les groupes d'homotopie des sphères en théorie des types homotopiques | |
Terminaison en présence de types dépendants et encodage par réécriture d’une théorie des types extensionelle avec polymorphisme d’univers. | |
Une théorie des constructions | |
A type theoretic approach to weak w-categories and related higher structures | |
Types for proofs and programs international workshop ; types '99, Lökeberg, Sweden, June 12 - 16, 1999 ; selected papers | |
TYPES'99 | |
Verified computing in homological algebra : a journey exploring the power and limits of dependent type theory |