Thierry Coquand

Coquand in 2006

Thierry Coquand (French: [kɔkɑ̃]; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg,[1] having previously worked at INRIA. He is known for his work in constructive mathematics, especially the calculus of constructions.

He received his Ph.D. under the supervision of Gérard Huet, another academic who has experience in both mathematics and computer science. According to the ACM Digital Library, his first published article was a 1985 collaboration with Huet titled "Constructions: A Higher Order Proof System for Mechanizing Mathematics".[2] Coquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics.[3] In the following year, 1986, Coquand published a noteworthy paper about Girard's paradox in the System U logic system.[4] Since then, Coquand has written a wide variety of papers in both French and English.

In addition to his contributions to theoretical computer science, Coquand is also known for being the co-creator of the Coq (the name partially being a reference to Coquand's surname) proof assistant, which he began development of in 1984 while working at INRIA (a French national research institute for computer science and mathematics), and which was officially released in 1989.[5] Coq won the ACM SIGPLAN Programming Languages Software Award in 2013, for "provid[ing] a rich environment for interactive development of machine-checked formal reasoning".[6][7] Coq has been used to provide novel solutions for mathematical problems, especially for those that have a non-surveyable proof, such as the four color theorem. It has also been used in software development, such as with the CompCert C compiler.[8]

Coquand often gives talks about the subjects that he specializes in, such as his description of the work of University of Nottingham professor Thorsten Altenkirch.[9]

See also

References

  1. ^ "Thierry Coquand". University of Gothenburg. Archived from the original on 27 March 2023. Retrieved 27 March 2023.
  2. ^ Constructions: A Higher Order Proof System for Mechanizing Mathematics. April 1985. pp. 151–184. ISBN 9783540159834. Archived from the original on 24 February 2023. Retrieved 24 February 2023.
  3. ^ Coquand, Thierry; Huet, Gérard (1985). "A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction". Journal of Symbolic Computation. 1 (3): 323–328. doi:10.1016/S0747-7171(85)80040-7. Archived from the original on 24 February 2023. Retrieved 24 February 2023.
  4. ^ "An analysis of Girard's paradox". Archived from the original on 24 February 2023. Retrieved 24 February 2023.
  5. ^ "What is Coq?". Archived from the original on 24 February 2023. Retrieved 24 February 2023.
  6. ^ "Coq received ACM SIGPLAN Programming Languages Software 2013 award". Archived from the original on 22 February 2023. Retrieved 22 February 2023.
  7. ^ "Programming Languages Software Award". Archived from the original on 25 February 2023. Retrieved 25 February 2023.
  8. ^ "Thierry Coquand". Archived from the original on 25 February 2023. Retrieved 25 February 2023.
  9. ^ "Paradoxes and Definitions" (PDF). Archived (PDF) from the original on 25 February 2023. Retrieved 25 February 2023.

Read other articles:

Junaedi (militer)

Junaedi Pa Sahli Tk. III Kasad Bidang PolkamnasMasa jabatan27 Juni 2022 – 29 Agustus 2022 PendahuluMohammad MunibPenggantiHarfendiWaaster Kasad Bidang Tahwil Komsos dan Bakti TNIMasa jabatan17 Nopember 2021 – 27 Juni 2022 PendahuluToto NurwantoPenggantiRudy Rachmat NugrahaKapok Sahli Pangdam I/Bukit BarisanMasa jabatan24 Maret 2021 – 17 Nopember 2021 PendahuluJohn SihombingPenggantiImmer Hotma Partogi ButarbutarKadep Oyu SeskoadMasa jabatan2020 – 24...

 

 

Holism in science

Approach to research that emphasizes the study of complex systems Holism in science, holistic science, or methodological holism is an approach to research that emphasizes the study of complex systems. Systems are approached as coherent wholes whose component parts are best understood in context and in relation to both each other and to the whole. Holism typically stands in contrast with reductionism, which describes systems by dividing them into smaller components in order to understand them ...

 

 

The Highwayman (novel)

This article is about the 2004 R. A. Salvatore novel. For other uses, see Highwayman (disambiguation). This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help to improve this article by introducing more precise citations. (December 2018) (Learn how and when to remove this template message) The Highwayman CoverAuthorR. A. SalvatoreCountryUnited StatesLanguageEnglishSeriesCoronaGenreFantasy/Eth...

Pembagian administratif Ceko

Region di Republik CekoKraje České republiky (Czech)KategoriNegara kesatuanLetakRepublik CekoJumlah wilayah14 RegionPenduduk310,245 (Karlovy Vary) – 1,274,633 (Central Bohemia)Luas500 km2 (192 sq mi) (Prague) - 1.101.500 km2 (425.290 sq mi) (Central Bohemia)PemerintahanRegionPembagian administratifDistrik Pembagian administratif Ceko terdiri atas 13 region dan 1 daerah ibu kota pada tingkat pertama serta 76 distrik region pada tingkat kedua.[1] Region...

 

 

Coppa Italia 1935-1936

Coppa Italia 1935-1936 Competizione Coppa Italia Sport Calcio Edizione 3ª Organizzatore Direttorio Divisioni Superiori Date dal 14 settembre 1935all'11 giugno 1936 Luogo  Italia Partecipanti 98 Sede finale Genova Risultati Vincitore Torino(1º titolo) Finalista Alessandria Semi-finalisti FiorentinaMilan Statistiche Miglior marcatore Pietro Buscaglia (8) Incontri disputati 102 Gol segnati 370 (3,63 per incontro) La formazione del Torino che si aggiudicò la coppa nazionale...

 

 

Anneville-Ambourville

Pour les articles homonymes, voir Anneville. Anneville-Ambourville Le manoir des templiers. Héraldique Administration Pays France Région Normandie Département Seine-Maritime Arrondissement Rouen Intercommunalité Métropole Rouen Normandie Maire Mandat Éric Lefebvre 2020-2026 Code postal 76480 Code commune 76020 Démographie Gentilé Annevillais Populationmunicipale 1 168 hab. (2021 ) Densité 57 hab./km2 Géographie Coordonnées 49° 27′ 44″ nord, 0°&#...

National Highway 317A (India)

National Highway in India National Highway 317AMap of the National Highway in redRoute informationPart of AH48 Length18.2 km (11.3 mi)Major junctionsSouth endHasimaraNorth endJaigaon LocationCountryIndiaStatesWest Bengal Highway system Roads in India Expressways National State Asian ← NH 317→ NH 317 National Highway 317A, commonly called NH 317A is a national highway in the state of West Bengal in India. It is a branch of National Highway 317.[1][2]...

 

 

Ida Ayu Nyoman Rai

Artikel atau bagian dari artikel ini menggunakan gaya bahasa naratif yang tidak sesuai dengan Wikipedia sehingga menurunkan kualitas artikel ini.Bantulah Wikipedia memperbaikinya. Setelah dirapikan, tolong hapus pesan ini. Ayu Nyoman RaiPotret Ayu Nyoman Rai bersama SoekarnoLahir1 Januari 1881Buleleng, Bali, Hindia BelandaMeninggal12 September 1958 (umur 77)Blitar, Jawa Timur, IndonesiaKebangsaanIndonesiaDikenal atasIbu dari SoekarnoSuami/istriRaden Soekemi Sosrodihardjo ​ ​&#...

 

 

ソー (オー＝ド＝セーヌ県)

Sceaux 行政国 フランス地域圏 (Région) イル＝ド＝フランス地域圏県 (département) オー＝ド＝セーヌ県郡 (arrondissement) アントニー郡小郡 (canton) 小郡庁所在地INSEEコード 92071郵便番号 92330市長（任期） フィリップ・ローラン（2008年-2014年）自治体間連合 (fr) メトロポール・デュ・グラン・パリ人口動態人口 19,679人（2007年）人口密度 5466人/km2住民の呼称 Scéens地理座標 北緯48度4...

John Murray Anderson

Canadian theatre director and producer Anderson c. 1915–20 John Murray Anderson (September 20, 1886 – January 30, 1954) was a Canadian theatre director and producer, songwriter, actor, screenwriter, dancer and lighting designer, who made his career in the United States, primarily in New York City and Hollywood. He worked in almost every genre of show business, including vaudeville, Broadway, and film. He also directed plays in London. Early life and education John Murray Anderson was born...

 

 

羅德島州

本條目存在以下問題，請協助改善本條目或在討論頁針對議題發表看法。 此條目需要擴充。 (2013年1月1日)请協助改善这篇條目，更進一步的信息可能會在討論頁或扩充请求中找到。请在擴充條目後將此模板移除。 此條目需要补充更多来源。 (2013年1月1日)请协助補充多方面可靠来源以改善这篇条目，无法查证的内容可能會因為异议提出而被移除。致使用者：请搜索一下条目的...

 

 

Neuropil

Type of area in the nervous system This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Neuropil – news · newspapers · books · scholar · JSTOR (April 2012) (Learn how and when to remove this message) NeuropilDetailsSystemNervous systemIdentifiersLatinneuropilusMeSHD019581THH2.00.06.2.02005 Anatomical terms of mic...

نيكس

نيكسمعلومات عامةجزء من نظام بلوتو الاسم الرسمي (134340) Plutó II (بالإنجليزية) سُمِّي باسم نكس المكتشف أو المخترع آلان ستيرنمرصد هابل الفضائي زمن الاكتشاف أو الاختراع 15 مايو 2005 موقع الاكتشاف الفلكي مرصد هابل الفضائي الجرم السماوي الأم بلوتو الانحراف المداري 0٫0023 زاوية الميلان 0٫...

 

 

Hexanchiformes

Order of sharks HexanchiformesTemporal range: Early Jurassic–Recent[1] PreꞒ Ꞓ O S D C P T J K Pg N Possible Permian record Broadnose sevengill shark (Notorynchus cepedianus) Frilled shark, (Chlamydoselachus anguineus) Scientific classification Domain: Eukaryota Kingdom: Animalia Phylum: Chordata Class: Chondrichthyes Subclass: Elasmobranchii Clade: Neoselachii Subdivision: Selachimorpha Superorder: Squalomorphii Order: HexanchiformesF. de Buen, 1926 Families †Paraorthacodontid...

 

 

18th-century history of Germany

Main articles: Early modern history of Germany and History of Germany Part of a series on the History of Germany Topics Chronology Historiography Military history Economic history Healthcare Islam LGBT history Jewish history Women's history Territorial evolution Historic states (Holy Roman Empire) Monarchs (Queens, Empresses, 1918, Family tree, Austria, Bavaria, Prussia, Saxony, Württemberg, Mediatised) Early history Germanic peoples Migration Period Barbarian kingdoms Frankish Empire Middl...

Stourbridge Lion

Railroad steam locomotive built in 1829 Stourbridge LionThe Stourbridge Lion's first run, as depicted by Clyde Osmer DeLand c. 1916Type and originPower typeSteamBuilderFoster, Rastrick and CompanyBuild date1829SpecificationsConfiguration:​ • Whyte0-4-0Gauge4 ft 3 in (1,295 mm)Driver dia.48 in (1.219 m)Loco weight14,000 lb (6,400 kg; 6.4 t)Tender weight5,800 lb (2,600 kg; 2.6 t)Total weight19,800 lb (9,000 ...

 

 

غاوريو (كيكلاديس)

غاوريو   تقسيم إداري البلد اليونان  [1] خصائص جغرافية إحداثيات 37°53′00″N 24°44′00″E / 37.88333333°N 24.73333333°E / 37.88333333; 24.73333333   الارتفاع 10 متر  السكان التعداد السكاني 849 (resident population of Greece) (2021)798 (resident population of Greece) (2001)570 (resident population of Greece) (1991)810 (resident population of Greece) (2011)3...

 

 

Transavia France

Low-cost airline of France This article is about the French airline. For its Dutch counterpart, see Transavia. Transavia France IATA ICAO Callsign TO TVF FRANCE SOLEIL Founded14 November 2006; 17 years ago (2006-11-14)Commenced operationsMay 2007; 17 years ago (2007-05)Operating basesLyonMontpellierNantesParis–OrlyFleet size73Destinations122[1]Parent companyAir France (95.5%)Transavia (4.5%)HeadquartersParay Vieille Poste, FranceKey peopleOli...

Netherlands national futsal team

NetherlandsShirt badge/Association crestNickname(s)OranjeHollandThe Flying Dutchmen A Clockwork Orange La Machina NaranjaAssociationRoyal Dutch Football AssociationConfederationUEFA (Europe)Head coach Miguel Andrés MorenoFIFA codeNEDFIFA ranking27 (December 2023)[1] Home colours Away colours First international Belgium 7–2 Netherlands (Genk, Belgium; 22 April 1977)Biggest win Netherlands 13–0 Estonia (Visoko, Bosnia and Herzegovina; 28 February 2008)Biggest d...

 

 

Minotaur

Creature of Greek mythology This article is about the mythological monster. For other uses, see Minotaur (disambiguation). MinotaurThe Minotaur, tondo of an Attic bilingual kylix from c. 515 BC.Other namesAsterionAbodeLabyrinth, CreteGenealogyParentsCretan Bull and PasiphaëSiblingsAcacallis, Ariadne, Androgeus, Glaucus, Deucalion, Phaedra, Xenodice and Catreus In Greek mythology, the Minotaur (/ˈmaɪnətɔːr, ˈmɪnətɔːr/ MY-nə-tor, MIN-ə-tor,[1] US: /ˈmɪnətɑːr, -o�...