This HTML5 document contains 87 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dcthttp://purl.org/dc/terms/
n27http://data.bnf.fr/ark:/12148/cb151164792#
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-cahttp://ca.dbpedia.org/resource/
dbpedia-kohttp://ko.dbpedia.org/resource/
dbpedia-eshttp://es.dbpedia.org/resource/
n23http://www.paultaylor.eu/stable/
n18http://g.co/kg/m/
dbpedia-ruhttp://ru.dbpedia.org/resource/
dbpedia-ukhttp://uk.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n31https://www.quora.com/topic/
category-frhttp://fr.dbpedia.org/resource/Catégorie:
dbpedia-plhttp://pl.dbpedia.org/resource/
dbpedia-pthttp://pt.dbpedia.org/resource/
n12http://fr.dbpedia.org/resource/Modèle:
dbpedia-cshttp://cs.dbpedia.org/resource/
wikipedia-frhttp://fr.wikipedia.org/wiki/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n22http://ma-graph.org/entity/
n13https://id.loc.gov/authorities/names/
dbpedia-zhhttp://zh.dbpedia.org/resource/
dbpedia-frhttp://fr.dbpedia.org/resource/
prop-frhttp://fr.dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbpedia-fr:Correspondance_de_Curry-Howard
rdfs:label
Izomorfizm Curry’ego-Howarda Curry-Howard-Isomorphismus カリー=ハワード同型対応 柯里-霍华德同构 Correspondance de Curry-Howard Curry–Howard correspondence Відповідність Каррі — Говарда
rdfs:comment
La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité. Ils établissent des relations entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, date à laquelle Haskell Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969 où William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul
rdfs:seeAlso
n31:Curry–Howard-Correspondence
owl:sameAs
dbr:Curry–Howard_correspondence dbpedia-ja:カリー=ハワード同型対応 dbpedia-cs:Curryho–Howardův_isomorfismus n13:sh2001002954 dbpedia-es:Correspondencia_de_Curry-Howard dbpedia-ko:커리-하워드_대응 n18:01lqbf dbpedia-uk:Відповідність_Каррі_—_Говарда dbpedia-zh:柯里-霍华德同构 dbpedia-ru:Соответствие_Карри_—_Ховарда n22:85343465 dbpedia-pt:Isomorfismo_de_Curry-Howard dbpedia-ca:Correspondència_Curry-Howard n27:about dbpedia-pl:Izomorfizm_Curry’ego-Howarda dbpedia-de:Curry-Howard-Isomorphismus wikidata:Q975734
dbo:wikiPageID
167076
dbo:wikiPageRevisionID
175623087
dbo:wikiPageWikiLink
dbpedia-fr:Haskell_Curry dbpedia-fr:Réalisabilité_classique dbpedia-fr:Théorie_de_la_calculabilité dbpedia-fr:Thierry_Coquand dbpedia-fr:Jean-Louis_Krivine category-fr:Théorie_de_la_démonstration dbpedia-fr:Système_de_gestion_d'exceptions dbpedia-fr:Brevet_logiciel dbpedia-fr:Nicolaas_Govert_de_Bruijn dbpedia-fr:Système_à_la_Hilbert dbpedia-fr:Logique_linéaire dbpedia-fr:Logique_mathématique dbpedia-fr:Isomorphisme dbpedia-fr:Logique_intuitionniste dbpedia-fr:Système_T dbpedia-fr:William_Alvin_Howard category-fr:Calculabilité dbpedia-fr:Arithmétique_du_second_ordre category-fr:Logique_mathématique dbpedia-fr:Logique_combinatoire dbpedia-fr:Système_T1 dbpedia-fr:Système_F dbpedia-fr:Kurt_Gödel dbpedia-fr:Sémantique_dénotationnelle dbpedia-fr:Jean-Yves_Girard dbpedia-fr:Théorème_de_complétude_de_Gödel dbpedia-fr:Informatique_théorique category-fr:Théorie_des_types dbpedia-fr:Lambda-calcul dbpedia-fr:Automath dbpedia-fr:Calcul_des_constructions dbpedia-fr:Joachim_Lambek dbpedia-fr:Calcul_des_séquents dbpedia-fr:Catégorie_cartésienne dbpedia-fr:Démonstration_automatique_de_théorèmes dbpedia-fr:Thoralf_Skolem dbpedia-fr:Théorèmes_d'incomplétude_de_Gödel dbpedia-fr:Fonction_récursive_primitive dbpedia-fr:Théorie_de_la_démonstration dbpedia-fr:Loi_de_Peirce dbpedia-fr:Réalisabilité dbpedia-fr:Stephen_Cole_Kleene dbpedia-fr:Déduction_naturelle dbpedia-fr:Déduction_modulo
dbo:wikiPageExternalLink
n23:Proofs%2BTypes.html
dbo:wikiPageLength
9684
dct:subject
category-fr:Logique_mathématique category-fr:Théorie_de_la_démonstration category-fr:Calculabilité category-fr:Théorie_des_types
prop-fr:wikiPageUsesTemplate
n12:Palette n12:References n12:Portail n12:Référence_nécessaire
prov:wasDerivedFrom
wikipedia-fr:Correspondance_de_Curry-Howard?oldid=175623087&ns=0
foaf:isPrimaryTopicOf
wikipedia-fr:Correspondance_de_Curry-Howard
dbo:namedAfter
dbpedia-fr:Haskell_Curry dbpedia-fr:William_Alvin_Howard
dbo:abstract
La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité. Ils établissent des relations entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, date à laquelle Haskell Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969 où William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul typé. La correspondance de Curry-Howard a joué un rôle important en logique, car elle a établi un pont entre théorie de la démonstration et informatique théorique. On la retrouve utilisée sous une forme ou une autre dans de très nombreux travaux allant des années 1960 à nos jours : sémantique dénotationnelle, logique linéaire, réalisabilité, démonstration automatique, etc.