Christine Paulin-Mohring

Christine Paulin-Mohring (born 1962)[1] is a mathematical logician and computer scientist, and Professor at Paris-Saclay University, best known for developing the interactive theorem prover Coq.

Christine Paulin-Mohring
Born1962 (1962)
Alma materParis Diderot University
Known forCoq
AwardsACM Software System Award (2013)
Scientific career
FieldsMathematics, computer science
InstitutionsParis-Saclay University
Doctoral advisorGérard Huet

Biography

Paulin-Mohring received her PhD in 1989 under the supervision of Gérard Huet.[2] She has been a professor at Paris-Saclay University since 1997 and the dean of the Paris-Saclay Faculty of Sciences since 2016.[3]

Between 2012 and 2015, she was the Scientific Coordinator of the Labex DigiCosme.[4] Currently, she is a member of the editorial board of the Journal of Formalized Reasoning.[5]

Recognition

Paulin-Mohring won the Michel-Monpetit Prize of the French Academy of Sciences in 2015.[6]

She and the rest of the Coq development team (Thierry Coquand, Gérard Huet, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran) won the 2013 ACM Software System Award awarded by the Association for Computing Machinery.

gollark: My tape download program now supports downloading big files without splitting them, via range requests, assuming they're served from a server which supports it: https://pastebin.com/LW9RFpmY (do `web2tape https://url.whatever range`)
gollark: Here is a similar thing for JSON. Note that it delegates out to an external JSON library for string escaping.```luafunction safe_json_serialize(x, prev) local t = type(x) if t == "number" then if x ~= x or x <= -math.huge or x >= math.huge then return tostring(x) end return string.format("%.14g", x) elseif t == "string" then return json.encode(x) elseif t == "table" then prev = prev or {} local as_array = true local max = 0 for k in pairs(x) do if type(k) ~= "number" then as_array = false break end if k > max then max = k end end if as_array then for i = 1, max do if x[i] == nil then as_array = false break end end end if as_array then local res = {} for i, v in ipairs(x) do table.insert(res, safe_json_serialize(v)) end return "["..table.concat(res, ",").."]" else local res = {} for k, v in pairs(x) do table.insert(res, json.encode(tostring(k)) .. ":" .. safe_json_serialize(v)) end return "{"..table.concat(res, ",").."}" end elseif t == "boolean" then return tostring(x) elseif x == nil then return "null" else return json.encode(tostring(x)) endend```
gollark: My tape shuffler thing from a while ago got changed round a bit. Apparently there's some demand for it, so I've improved the metadata format and written some documentation for it, and made the encoder work better by using file metadata instead of filenames and running tasks in parallel so it's much faster. The slightly updated code and docs are here: https://pastebin.com/SPyr8jrh. There are also people working on alternative playback/encoding software for the format for some reason.
gollark: Are you less utilitarian with your names than <@125217743170568192> but don't really want to name your cool shiny robot with the sort of names used by *foolish organic lifeforms*? Care somewhat about storage space and have HTTP enabled to download name lists? Try OC Robot Name Thing! It uses the OpenComputers robot name list for your... CC computer? https://pastebin.com/PgqwZkn5
gollark: I wanted something to play varying music in my base, so I made this.https://pastebin.com/SPyr8jrh is the CC bit, which automatically loads random tapes from a connected chest into the connected tape drive and plays a random track. The "random track" bit works by using an 8KiB block of metadata at the start of the tape.Because I did not want to muck around with handling files bigger than CC could handle within CC, "tape images" are generated with this: https://pastebin.com/kX8k7xYZ. It requires `ffmpeg` to be available and `LionRay.jar` in the working directory, and takes one command line argument, the directory to load to tape. It expects a directory of tracks in any ffmpeg-compatible audio format with the filename `[artist] - [track].[filetype extension]` (this is editable if you particularly care), and outputs one file in the working directory, `tape.bin`. Please make sure this actually fits on your tape.I also wrote this really simple program to write a file from the internet™️ to tape: https://pastebin.com/LW9RFpmY. You can use this to write a tape image to tape.EDIT with today's updates: the internet→tape writer now actually checks if the tape is big enough, and the shuffling algorithm now actually takes into account tapes with different numbers of tracks properly, as well as reducing the frequency of a track after it's already been played recently.

References
  1. Birth year from Library of Congress catalog entry. Retrieved 1 December 2018.
  2. Christine Paulin-Mohring at the Mathematics Genealogy Project
  3. "Short biography". Laboratoire de Recherche en Informatique. Retrieved 11 May 2020.
  4. "Labex DigiCosme | Organisation-EN". DigiCosme - Paris-Saclay. Archived from the original on 19 August 2017. Retrieved 10 October 2018.
  5. "Editorial Team". Journal of Formalized Reasoning. Retrieved 10 October 2018.
  6. "Lauréats 2015 des prix thématiques" (in French). French Academy of Sciences. Retrieved 29 May 2019.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.