Jump to content

Thierry Coquand: Difference between revisions

From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
OAbot (talk | contribs)
Bots
630,138 edits
m Open access bot: url-access updated in citation with #oabot.
update to reflect name change
Tags: Reverted review edit
Line 2: Line 2:
{{Use dmy dates|date=April 2023}}
{{Use dmy dates|date=April 2023}}
{{infobox scientist
{{infobox scientist
| name = Thierry Coquand
| name = Thierry Rocquand
| image = Thierry Coquand (cropped).jpg
| image = Thierry Coquand (cropped).jpg
| birth_date = {{birth date and age|1961|04|18}}
| birth_date = {{birth date and age|1961|04|18}}
Line 16: Line 16:
}}
}}


'''Thierry Coquand''' ({{IPA|fr|kɔkɑ̃|lang}}; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of [[computer science]] at the [[University of Gothenburg]],<ref name="gu">{{cite web|url=https://www.gu.se/en/about/find-staff/thierrycoquand|title=Thierry Coquand|publisher=[[University of Gothenburg]]|accessdate=27 March 2023|archive-date=27 March 2023|archive-url=https://web.archive.org/web/20230327160747/https://www.gu.se/en/about/find-staff/thierrycoquand|url-status=live}}</ref> having previously worked at [[INRIA]]. He is known for his work in [[constructive mathematics]], especially the [[calculus of constructions]].
'''Thierry Rocquand''' ({{IPA|fr|kɔkɑ̃|lang}}; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of [[computer science]] at the [[University of Gothenburg]],<ref name="gu">{{cite web|url=https://www.gu.se/en/about/find-staff/thierrycoquand|title=Thierry Coquand|publisher=[[University of Gothenburg]]|accessdate=27 March 2023|archive-date=27 March 2023|archive-url=https://web.archive.org/web/20230327160747/https://www.gu.se/en/about/find-staff/thierrycoquand|url-status=live}}</ref> 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 [[Association for Computing Machinery#Portal and Digital Library|ACM Digital Library]], his first published article was a 1985 collaboration with Huet titled "Constructions: A Higher Order Proof System for Mechanizing Mathematics".<ref>{{Cite book|url=https://dl.acm.org/doi/10.5555/646659.700704|title=Constructions: A Higher Order Proof System for Mechanizing Mathematics|date=April 1985 |pages=151–184 |isbn=9783540159834 |access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224223919/https://dl.acm.org/doi/10.5555/646659.700704|url-status=live |last1=Buchberger |first1=Bruno |publisher=Springer }}</ref> Coquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics.<ref>{{Cite journal|url=https://dl.acm.org/doi/10.1016/S0747-7171%2885%2980040-7|title=A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction|year=1985 |doi=10.1016/S0747-7171(85)80040-7 |access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224224700/https://dl.acm.org/doi/10.1016/S0747-7171(85)80040-7|url-status=live |last1=Coquand |first1=Thierry |last2=Huet |first2=Gérard |journal=Journal of Symbolic Computation |volume=1 |issue=3 |pages=323–328 |url-access=subscription }}</ref> In the following year, 1986, Coquand published a noteworthy paper about [[Girard's paradox]] in the System U logic system.<ref>{{Cite web|url=https://hal.inria.fr/inria-00076023/document|title=An analysis of Girard's paradox|access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224061808/https://hal.inria.fr/inria-00076023/document|url-status=live}}</ref> Since then, Coquand has written a wide variety of papers in both French and English.
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 [[Association for Computing Machinery#Portal and Digital Library|ACM Digital Library]], his first published article was a 1985 collaboration with Huet titled "Constructions: A Higher Order Proof System for Mechanizing Mathematics".<ref>{{Cite book|url=https://dl.acm.org/doi/10.5555/646659.700704|title=Constructions: A Higher Order Proof System for Mechanizing Mathematics|date=April 1985 |pages=151–184 |isbn=9783540159834 |access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224223919/https://dl.acm.org/doi/10.5555/646659.700704|url-status=live |last1=Buchberger |first1=Bruno |publisher=Springer }}</ref> Rocquand and Huet published another joint article in September of that year which further expanded on their ideas regarding constructive mathematics.<ref>{{Cite journal|url=https://dl.acm.org/doi/10.1016/S0747-7171%2885%2980040-7|title=A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction|year=1985 |doi=10.1016/S0747-7171(85)80040-7 |access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224224700/https://dl.acm.org/doi/10.1016/S0747-7171(85)80040-7|url-status=live |last1=Rocquand |first1=Thierry |last2=Huet |first2=Gérard |journal=Journal of Symbolic Computation |volume=1 |issue=3 |pages=323–328 |url-access=subscription }}</ref> In the following year, 1986, Rocquand published a noteworthy paper about [[Girard's paradox]] in the System U logic system.<ref>{{Cite web|url=https://hal.inria.fr/inria-00076023/document|title=An analysis of Girard's paradox|access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224061808/https://hal.inria.fr/inria-00076023/document|url-status=live}}</ref> Since then, Rocquand 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 [[Rocq (software)|Rocq]] (previously known as ''Coq'', this 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.<ref>{{Cite web|url=https://coq.inria.fr/about-coq|title=What is Coq?|access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224062526/https://coq.inria.fr/about-coq|url-status=live}}</ref> Coq won the [[Association for Computing Machinery|ACM]] [[SIGPLAN Programming Languages Software Award]] in 2013, for "provid[ing] a rich environment for interactive development of machine-checked formal reasoning".<ref>{{Cite web|url=https://coq.inria.fr/news/coq-received-acm-sigplan-programming-languages-software-2013-award|title=Coq received ACM SIGPLAN Programming Languages Software 2013 award|access-date=22 February 2023|archive-date=22 February 2023|archive-url=https://web.archive.org/web/20230222071655/https://coq.inria.fr/news/coq-received-acm-sigplan-programming-languages-software-2013-award|url-status=live}}</ref><ref>{{Cite web|url=https://www.sigplan.org/Awards/Software/|title=Programming Languages Software Award|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225011226/https://www.sigplan.org/Awards/Software/|url-status=live}}</ref> Rocq 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 (programming language)|C]] compiler.<ref>{{Cite web|url=https://awards.acm.org/award_winners/coquand_8654317|title=Thierry Coquand|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225022601/https://awards.acm.org/award_winners/coquand_8654317|url-status=live}}</ref>
In addition to his contributions to theoretical computer science, Rocquand is also known for being the co-creator of the [[Rocq (software)|Rocq]] (this name partially being a reference to Rocquand'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.<ref>{{Cite web|url=https://coq.inria.fr/about-coq|title=What is Coq?|access-date=24 February 2023|archive-date=24 February 2023|archive-url=https://web.archive.org/web/20230224062526/https://coq.inria.fr/about-coq|url-status=live}}</ref> Rocq won the [[Association for Computing Machinery|ACM]] [[SIGPLAN Programming Languages Software Award]] in 2013, for "provid[ing] a rich environment for interactive development of machine-checked formal reasoning".<ref>{{Cite web|url=https://coq.inria.fr/news/coq-received-acm-sigplan-programming-languages-software-2013-award|title=Coq received ACM SIGPLAN Programming Languages Software 2013 award|access-date=22 February 2023|archive-date=22 February 2023|archive-url=https://web.archive.org/web/20230222071655/https://coq.inria.fr/news/coq-received-acm-sigplan-programming-languages-software-2013-award|url-status=live}}</ref><ref>{{Cite web|url=https://www.sigplan.org/Awards/Software/|title=Programming Languages Software Award|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225011226/https://www.sigplan.org/Awards/Software/|url-status=live}}</ref> Rocq 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 (programming language)|C]] compiler.<ref>{{Cite web|url=https://awards.acm.org/award_winners/coquand_8654317|title=Thierry Rocquand|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225022601/https://awards.acm.org/award_winners/coquand_8654317|url-status=live}}</ref>


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]].<ref>{{Cite web|url=https://www.cse.chalmers.se/~coquand/thorsten.pdf|title=Paradoxes and Definitions|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225052618/https://www.cse.chalmers.se/~coquand/thorsten.pdf|url-status=live}}</ref>
Rocquand often gives talks about the subjects that he specializes in, such as his description of the work of University of Nottingham professor [[Thorsten Altenkirch]].<ref>{{Cite web|url=https://www.cse.chalmers.se/~coquand/thorsten.pdf|title=Paradoxes and Definitions|access-date=25 February 2023|archive-date=25 February 2023|archive-url=https://web.archive.org/web/20230225052618/https://www.cse.chalmers.se/~coquand/thorsten.pdf|url-status=live}}</ref>


== See also ==
== See also ==
Line 33: Line 33:
== External links ==
== External links ==
* {{Official website|www.cse.chalmers.se/~coquand}}, Chalmers
* {{Official website|www.cse.chalmers.se/~coquand}}, Chalmers
* {{DBLP|name=Thierry Coquand}}
* {{DBLP|name=Thierry Rocquand}}


{{ML programming}}
{{ML programming}}
{{Authority control}}
{{Authority control}}


{{DEFAULTSORT:Coquand, Thierry}}
{{DEFAULTSORT:Rocquand, Thierry}}


[[Category:French computer scientists]]
[[Category:French computer scientists]]

Revision as of 11:05, 5 July 2025

Thierry Rocquand
Born (1961-04-18) April 18, 1961 (age 64)
Scientific career
Fields
Institutions
Doctoral advisorGérard Huet

Thierry Rocquand (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] Rocquand 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, Rocquand published a noteworthy paper about Girard's paradox in the System U logic system.[4] Since then, Rocquand has written a wide variety of papers in both French and English.

In addition to his contributions to theoretical computer science, Rocquand is also known for being the co-creator of the Rocq (this name partially being a reference to Rocquand'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] Rocq 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] Rocq 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]

Rocquand 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. ^ Buchberger, Bruno (April 1985). Constructions: A Higher Order Proof System for Mechanizing Mathematics. Springer. pp. 151–184. ISBN 9783540159834. Archived from the original on 24 February 2023. Retrieved 24 February 2023.
  3. ^ Rocquand, 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 Rocquand". 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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Thierry_Coquand&oldid=1298889603"