-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
82 lines (82 loc) · 9.55 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Jean Pichon-Pharabod</title>
<link rel="stylesheet" type="text/css" href="style.css"/>
</head>
<body>
<h1>Jean Pichon-Pharabod</h1>
<img style="float: right; display:block; width: 150px; margin-left: 1em;" src="https://pure.au.dk/portal/files-asset/305100958/CS2023_Jean_Pichon_web.jpg?w=320" />
<p>Tenure-track assistant professor in the <a href="https://cs.au.dk/research/logic-and-semantics">Logic & Semantics group</a> at the <a href="https://cs.au.dk/">Institut for Datalogi</a> of <a href="https://international.au.dk/">Aarhus University</a>.<br/>
<span class="old">Before that, I was a <a href="https://www.cam.ac.uk/research-staff/employment-and-career-management/employment-and-career-management-scheme/researchers-employment-policies-and-protocols/job-titles-and-duties">Research associate</a> in <a href="http://www.cl.cam.ac.uk/~pes20/">Peter Sewell</a>'s group at the <a href="http://www.cl.cam.ac.uk/">Computer Laboratory</a> of the <a href="http://www.cam.ac.uk/">University of Cambridge</a>, working on the <a href="http://www.cl.cam.ac.uk/~pes20/rems/">REMS</a> project, and an affiliated lecturer.</span><br/>
<span class="old">Before that, I was a PhD student supervised by <a href="http://www.cl.cam.ac.uk/~pes20/">Peter Sewell</a>.</span>
</p>
<h2>Contact</h2>
<p>jean.pichon at cs.au.dk<br/>
Office: Turing 129 (building 5341)<br/>
<a href="https://scholar.google.com/citations?user=ReYyKJAAAAAJ">Google Scholar</a><br/>
orcid: <a href="https://orcid.org/0000-0002-4442-6543">0000-0002-4442-6543</a><br/>
<a href="https://pure.au.dk/portal/en/persons/jean-yves-alexis-pichon(7705419e-fa64-4319-b0c1-da0f61ad128c).html">institutional webpage</a><br/>
<a href="https://www.linkedin.com/in/jean-pichon-pharabod-859569305/">LinkedIn page</a>
</p>
<h2>Research interests</h2>
<p>I am interested in bridging the gap between programming language theory and the industrial practice of programming with real-world systems, focusing in particular on relaxed memory concurrency and systems programming, from modelling and tooling to developing new reasoning methods</p>
<p>I am looking for motivated <a href="https://cs.au.dk/education/phd">PhD students</a>, PostDocs, and interns.</p>
<h2>Students</h2>
<ul>
<li><a href="https://cs.au.dk/~zyliu/">Zongyuan Liu</a> started 2020</li>
<li><a href="https://pure.au.dk/portal/da/persons/maxime%40cs.au.dk">Maxime Legoupil</a> started 2022</li>
<li><a href="https://junerousseau.github.io/">June Rousseau</a> started 2022</li>
</ul>
<h2>Funding</h2>
<ul>
<li><a href="https://www.amazon.science/research-awards/recipients/jean-pichon-pharabod">Amazon ARC Award 2024</a></li>
<li><a href="https://security.googleblog.com/2018/12/aspire-to-keep-protecting-billions-of.html">Google ASPIRE 2023 award</a></li>
<li><a href="https://security.googleblog.com/2018/12/aspire-to-keep-protecting-billions-of.html">Google ASPIRE 2022 award</a></li>
<li><a href="https://security.googleblog.com/2018/12/aspire-to-keep-protecting-billions-of.html">Google ASPIRE 2021 award</a></li>
<li><a href="https://auff.au.dk/bevillinger/auff-recruiting-grants">AUFF Starting Grant</a></li>
</ul>
<h2>Outreach</h2>
<p><a href="https://www.cl.cam.ac.uk/~jp622/reactive-scratch/">Reactive Scratch</a>: helping children learn programming using the <a href="https://en.wikipedia.org/wiki/Esterel">technology of the 80s</a> (rather than <a href="https://en.wikipedia.org/wiki/Structured_programming">that of the 60s</a>).</p>
<h2>Teaching</h2>
<ul>
<li>2nd year Computer Architecture, Operating Systems and Networks</li>
<li>3rd year Compilers</li>
<li>Master's Advanced Topics in Programming Language Theory</li>
<li><span class="old">Cambridge Part II (3rd year) <a href="https://www.cl.cam.ac.uk/teaching/2021/HLog+ModC/">Hoare Logic & Model Checking</a></span></li>
</ul>
<h2>Student projects</h2>
<p><a href="https://www.cl.cam.ac.uk/~jp622/student_projects.html">Student projects</a></p>
<h2>Software</h2>
<ul>
<li><a href="http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/">CppMem</a>, an interactive C/C++ memory model explorer</li>
<li><a href="http://cerberus.cl.cam.ac.uk/bmc.html">Cerberus-BMC</a>, an executable semantics for a substantial fragment of C</li>
<li><a href="https://www.cl.cam.ac.uk/~sf502/regressions/rmem/">rmem</a>, an interactive ISA and memory model explorer</li>
<li><a href="https://github.com/WasmCert/WasmCert-Coq">wasm_coq</a>, a Coq formalisation of WebAssembly 1.0 (based on <a href="https://www.isa-afp.org/entries/WebAssembly.html">C. Watt's WebAssembly semantics in Isabelle</a>)</li>
<li><a href="https://github.com/womeier/certicoqwasm/">CertiCoq-Wasm</a> (student project) <a href="https://www.cl.cam.ac.uk/~jp622/certicoq-wasm.pdf">pdf</a></li>
</ul>
<h2 id="publications">Publications</h2>
<p>See <a href="https://dblp.uni-trier.de/pers/hd/p/Pichon=Pharabod:Jean">DBLP</a>.</p>
<ul>
<li><span class="title">Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly</span>, Maxime Legoupil, June Rousseau, Aina Linn Georges, Jean Pichon-Pharabod, Lars Birkedal, in OOPSLA 2024 <a href="https://www.cl.cam.ac.uk/~jp622/iris-mswasm.pdf">pdf</a></li>
<li><span class="title">An axiomatic basis for computer programming on the relaxed Arm-A architecture: The AxSL Logic</span>, Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod, in POPL 2024 <a href="https://www.cl.cam.ac.uk/~jp622/axsl.pdf">pdf</a></li>
<li><span class="title">VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A</span>, Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, and Lars Birkedal, in PLDI 2023 <a href="https://www.cl.cam.ac.uk/~jp622/vmsl.pdf">pdf</a></li>
<li><span class="title">Iris-Wasm: Robust and Modular Verification of WebAssembly Programs</span>, Xiaojia Rao, Aïna Linn Georges, Conrad Watt, Maxime Legoupil, Jean Pichon-Pharabod, Philippa Gardner, and Lars Birkedal, in PLDI 2023 <a href="https://www.cl.cam.ac.uk/~jp622/iris-wasm.pdf">pdf</a></li>
<li><span class="title">Islaris: Verification of Machine Code Against Authoritative ISA Semantics</span>, Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell, in PLDI 2022 <a href="https://www.cl.cam.ac.uk/~jp622/islaris.pdf">pdf</a></li>
<li><span class="title">Relaxed virtual memory in Armv8-A</span>, Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell, in ESOP 2022 <a href="https://www.cl.cam.ac.uk/~jp622/vmsa.pdf">pdf</a></li>
<li><span class="title">Two Mechanisations of WebAssembly 1.0</span>, Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner, in FM 2021 <a href="https://www.cl.cam.ac.uk/~jp622/two_wasm.pdf">pdf</a></li>
<li><span class="title">Repairing and Mechanising the JavaScript Relaxed Memory Model</span>, Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-yu Guo, in PLDI 2020 <a href="https://www.cl.cam.ac.uk/~jp622/repairing_javascript.pdf">pdf</a></li>
<li><span class="title">ARMv8-A system semantics: instruction fetch in relaxed architectures</span>, Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell, in ESOP 2020 <a href="https://www.cl.cam.ac.uk/~jp622/ifetch.pdf">pdf</a></li>
<li><span class="title">Weakening WebAssembly</span>, Conrad Watt, Andreas Rossberg, Jean Pichon-Pharabod, in OOPSLA 2019 <a href="https://www.cl.cam.ac.uk/~jp622/weakening_webassembly.pdf">pdf</a></li>
<li><span class="title">Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C</span>, Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell, in CAV 2019 <a href="https://www.cl.cam.ac.uk/~jp622/cerberus-bmc.pdf">pdf</a></li>
<li><span class="title">Promising-ARM/RISC-V: a simpler and faster operational concurrency model</span>, Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur, in PLDI 2019 <a href="https://www.cl.cam.ac.uk/~jp622/promising-arm-riscv.pdf">pdf</a></li>
<li><span class="title">A separation logic for a promising semantics</span>, Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis, in ESOP 2018 <a href="https://www.cl.cam.ac.uk/~jp622/sep_promising.pdf">pdf</a></li>
<li><span class="title">A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions</span>, Jean Pichon-Pharabod and Peter Sewell, in POPL 2016 <a href="https://www.cl.cam.ac.uk/~jp622/thin-air.pdf">pdf</a></li>
<li><span class="title">A Separation Logic for Fictional Sequential Consistency</span>, Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod, in ESOP 2015 <a href="https://www.cl.cam.ac.uk/~jp622/icap-tso.pdf">pdf</a></li>
<li><span class="title">The Problem of Programming Language Concurrency Semantics</span>, Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell, in ESOP 2015 <a href="https://www.cl.cam.ac.uk/~jp622/the_problem.pdf">pdf</a></li>
</ul>
<p>Thesis: <span class="title">A no-thin-air memory model for programming languages</span>, Jean Pichon-Pharabod <a href="https://www.repository.cam.ac.uk/handle/1810/274465">webpage</a></p>
<p>Last modified: 11 Dec 2024</p>
</body>
</html>