| Property |
Value |
| dbo:abstract
|
- En informatique théorique, la coinduction est une technique de définition et de vérification de propriétés de systèmes d'objets en interaction. La coinduction est la notion duale de l'induction structurelle. Les types définis par coinduction sont aussi connus comme codata et sont en général des structures de données infinie, tels que les flux. En tant que définition ou spécification informatique, la coinduction décrit comment un objet peut être décomposé en objets plus simples. Comme technique de démonstration, elle peut être utilisée pour montrer qu'une équation est satisfaite par toutes les implémentations possible d'une telle spécification. Pour engendrer et manipuler des codata, on utilise typiquement des fonctions corécursives en conjonction avec l'évaluation paresseuse. De manière informelle, plutôt que de définir une fonction par pattern-matching sur chacun de ses constructeurs inductifs, on définit des destructeurs (c'est le dual d'un constructeur). Pour une liste par exemple, les constructeurs sont nil et cons, les destructeurs sont tête et queue. En programmation, la coinduction, aussi appelée programmation co-logique, est une généralisation naturelle de la programmation logique à la programmation en logique coinductive, généralisant d'autres extensions, comme les arbres infinis, les prédicats paresseux, ou les prédicats communicants concurrents. Elle intervient en plus dans la vérification de propriétés infinitaires, le model checking, preuves par bisimilarité. En France, Claude Pair est un pionnier de l'utilisation de la coinduction en informatique. La coinduction est largement utilisée dans des assistants de preuves comme Coq. (fr)
- En informatique théorique, la coinduction est une technique de définition et de vérification de propriétés de systèmes d'objets en interaction. La coinduction est la notion duale de l'induction structurelle. Les types définis par coinduction sont aussi connus comme codata et sont en général des structures de données infinie, tels que les flux. En tant que définition ou spécification informatique, la coinduction décrit comment un objet peut être décomposé en objets plus simples. Comme technique de démonstration, elle peut être utilisée pour montrer qu'une équation est satisfaite par toutes les implémentations possible d'une telle spécification. Pour engendrer et manipuler des codata, on utilise typiquement des fonctions corécursives en conjonction avec l'évaluation paresseuse. De manière informelle, plutôt que de définir une fonction par pattern-matching sur chacun de ses constructeurs inductifs, on définit des destructeurs (c'est le dual d'un constructeur). Pour une liste par exemple, les constructeurs sont nil et cons, les destructeurs sont tête et queue. En programmation, la coinduction, aussi appelée programmation co-logique, est une généralisation naturelle de la programmation logique à la programmation en logique coinductive, généralisant d'autres extensions, comme les arbres infinis, les prédicats paresseux, ou les prédicats communicants concurrents. Elle intervient en plus dans la vérification de propriétés infinitaires, le model checking, preuves par bisimilarité. En France, Claude Pair est un pionnier de l'utilisation de la coinduction en informatique. La coinduction est largement utilisée dans des assistants de preuves comme Coq. (fr)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 4563 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| prop-fr:année
|
- 1997 (xsd:integer)
- 2007 (xsd:integer)
- 2011 (xsd:integer)
- 2012 (xsd:integer)
- 2015 (xsd:integer)
- 2016 (xsd:integer)
- October 2016 (fr)
|
| prop-fr:auteur
|
- Bart Jacobs (fr)
- Davide Sangiorgi (fr)
- Eduardo Giménez et Pierre Castéran (fr)
- Jan Rutten (fr)
- Pierre-Marie Pédrot (fr)
- Bart Jacobs (fr)
- Davide Sangiorgi (fr)
- Eduardo Giménez et Pierre Castéran (fr)
- Jan Rutten (fr)
- Pierre-Marie Pédrot (fr)
|
| prop-fr:collection
|
- Cambridge Tracts in Theoretical Computer Science (fr)
- Cambridge Tracts in Theoretical Computer Science (fr)
|
| prop-fr:consultéLe
| |
| prop-fr:isbn
| |
| prop-fr:issn
| |
| prop-fr:jour
| |
| prop-fr:journal
|
- Bulletin EATCS (fr)
- Mathematical Structures in Computer Science (fr)
- Bulletin EATCS (fr)
- Mathematical Structures in Computer Science (fr)
|
| prop-fr:langue
| |
| prop-fr:lieu
|
- Cambridge (fr)
- Cambridge (fr)
|
| prop-fr:mois
| |
| prop-fr:nom
|
- Silva (fr)
- Kozen (fr)
- Silva (fr)
- Kozen (fr)
|
| prop-fr:numéro
|
- 7 (xsd:integer)
- 62 (xsd:integer)
|
| prop-fr:pages
|
- 222 (xsd:integer)
- 1132 (xsd:integer)
|
| prop-fr:pagesTotales
| |
| prop-fr:prénom
|
- Dexter (fr)
- Alexandra (fr)
- Dexter (fr)
- Alexandra (fr)
|
| prop-fr:présentationEnLigne
| |
| prop-fr:sousTitre
|
- Towards Mathematics of States and Observation (fr)
- Towards Mathematics of States and Observation (fr)
|
| prop-fr:titre
|
- "A Tutorial on [Co-]Inductive Types in Coq" (fr)
- A Survey of coinduction in Coq (fr)
- A Tutorial on Algebras and Induction (fr)
- Advanced Topics in Bisimulation and Coinduction (fr)
- Introduction to Bisimulation and Coinduction (fr)
- Introduction to Coalgebra (fr)
- Practical coinduction (fr)
- "A Tutorial on [Co-]Inductive Types in Coq" (fr)
- A Survey of coinduction in Coq (fr)
- A Tutorial on Algebras and Induction (fr)
- Advanced Topics in Bisimulation and Coinduction (fr)
- Introduction to Bisimulation and Coinduction (fr)
- Introduction to Coalgebra (fr)
- Practical coinduction (fr)
|
| prop-fr:url
| |
| prop-fr:volume
| |
| prop-fr:wikiPageUsesTemplate
| |
| prop-fr:éditeur
|
- Cambridge University Press (fr)
- Cambridge University Press (fr)
|
| dct:subject
| |
| rdfs:comment
|
- En informatique théorique, la coinduction est une technique de définition et de vérification de propriétés de systèmes d'objets en interaction. La coinduction est la notion duale de l'induction structurelle. Les types définis par coinduction sont aussi connus comme codata et sont en général des structures de données infinie, tels que les flux. En France, Claude Pair est un pionnier de l'utilisation de la coinduction en informatique. La coinduction est largement utilisée dans des assistants de preuves comme Coq. (fr)
- En informatique théorique, la coinduction est une technique de définition et de vérification de propriétés de systèmes d'objets en interaction. La coinduction est la notion duale de l'induction structurelle. Les types définis par coinduction sont aussi connus comme codata et sont en général des structures de données infinie, tels que les flux. En France, Claude Pair est un pionnier de l'utilisation de la coinduction en informatique. La coinduction est largement utilisée dans des assistants de preuves comme Coq. (fr)
|
| rdfs:label
|
- Coinduction (fr)
- Коиндукция (ru)
- Coinduction (fr)
- Коиндукция (ru)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:knownFor
of | |
| is dbo:wikiPageWikiLink
of | |
| is prop-fr:domaines
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
