initial commit
This commit is contained in:
commit
bf34e8e676
|
|
@ -0,0 +1,22 @@
|
|||
BUILD_DIR := ./build
|
||||
SRCS := src/build.py src/index.html src/index.md src/assets/theme.css
|
||||
|
||||
.PHONY: all clean publish serve
|
||||
|
||||
site.tgz: $(SRCS)
|
||||
mkdir -p $(BUILD_DIR)
|
||||
python3 src/build.py > $(BUILD_DIR)/index.html
|
||||
cp -r src/assets $(BUILD_DIR)
|
||||
cd $(BUILD_DIR) && tar -cvzf ../site.tgz .
|
||||
|
||||
publish: site.tgz
|
||||
hut pages publish -d peio.scryk.net site.tgz
|
||||
|
||||
serve: site.tgz
|
||||
cd $(BUILD_DIR) && python3 -m http.server
|
||||
|
||||
clean:
|
||||
rm -rf $(BUILD_DIR)
|
||||
rm site.tgz
|
||||
|
||||
all: site.tgz
|
||||
|
|
@ -0,0 +1,54 @@
|
|||
body {
|
||||
font-family: sans-serif;
|
||||
font-size: 14px;
|
||||
line-height: 1.54;
|
||||
max-width: 700px;
|
||||
margin: 40px auto;
|
||||
padding: 2em;
|
||||
}
|
||||
|
||||
h1, h2, h3, nav a, dt {
|
||||
font-family: monospace;
|
||||
font-weight: 500;
|
||||
text-transform: uppercase;
|
||||
letter-spacing: 0.1rem;
|
||||
}
|
||||
|
||||
body img {
|
||||
height: 150px;
|
||||
border-radius: 20%;
|
||||
}
|
||||
|
||||
nav a {
|
||||
text-align: center;
|
||||
padding: 0px 16px;
|
||||
text-decoration: none;
|
||||
font-size: 17px;
|
||||
opacity: .7;
|
||||
}
|
||||
|
||||
nav a:hover {
|
||||
opacity: 1
|
||||
}
|
||||
|
||||
dl {
|
||||
display: flex;
|
||||
flex-flow: row wrap;
|
||||
}
|
||||
dt {
|
||||
flex-basis: 20%;
|
||||
padding: 2px 4px;
|
||||
text-align: right;
|
||||
}
|
||||
dd {
|
||||
flex-basis: 70%;
|
||||
flex-grow: 1;
|
||||
margin: 0;
|
||||
padding: 2px 4px;
|
||||
}
|
||||
|
||||
hr {
|
||||
border: none;
|
||||
border-top: 1px solid;
|
||||
margin: 2em auto;
|
||||
}
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
from os.path import abspath, dirname, join
|
||||
from jinja2 import Environment, FileSystemLoader, select_autoescape
|
||||
from markdown import markdown
|
||||
|
||||
here = dirname(abspath(__file__))
|
||||
|
||||
env = Environment(loader=FileSystemLoader(here), autoescape=False)
|
||||
index_tmpl = env.get_template('index.html')
|
||||
|
||||
with open(here + '/index.md') as fd:
|
||||
index_md = fd.read()
|
||||
content = markdown(index_md, extensions=['smarty', 'def_list', 'attr_list'])
|
||||
|
||||
print(index_tmpl.render(content=content))
|
||||
|
|
@ -0,0 +1,28 @@
|
|||
<!doctype html>
|
||||
<html>
|
||||
<head>
|
||||
<meta charset="utf8">
|
||||
<title>Peio Borthelle</title>
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
|
||||
<meta name="theme-color" content="#000000">
|
||||
<meta name="robots" content="index, follow">
|
||||
<meta property="og:title" content="Peio Borthelle">
|
||||
<meta property="og:description" content="Professional page of Peio Borthelle">
|
||||
<link rel="stylesheet" href="/assets/theme.css">
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<a href="/#contact">contact</a>
|
||||
<a href="/#events">events</a>
|
||||
<a href="/#interests">interests</a>
|
||||
<a href="/#pubs">publications</a>
|
||||
</nav>
|
||||
<main>
|
||||
{{ content }}
|
||||
</main>
|
||||
<hr>
|
||||
<footer>
|
||||
2024 · <a href="https://creativecommons.org/licenses/by-nc/2.0/">CC BY-NC 2.0</a> · Thanks to my buddy <a href="https://lucas.escot.me">Lucas Escot</a> for some CSS · This was not generated by <a href="https://achille.acatalepsie.fr/">achille</a>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,99 @@
|
|||
# Peio Borthelle
|
||||
|
||||
I am currently a PhD student, under the supervision of [Tom
|
||||
Hirschowitz](https://hirschowitz.pages.math.cnrs.fr/), [Guilhem
|
||||
Jaber](https://guilhem.jaber.fr/) and [Yannick
|
||||
Zakowski](https://perso.ens-lyon.fr/yannick.zakowski/). I am located at
|
||||
[Université Savoie Mont Blanc](https://www.univ-smb.fr/) in Chambéry, France, more specifically in
|
||||
the LIMD (logic, computer science and discrete math) team of the
|
||||
[LAMA](https://www.lama.univ-smb.fr/) (math lab).
|
||||
|
||||
## Contact {: #contact}
|
||||
|
||||
E-Mail
|
||||
: [`peio.borthelle@univ-smb.fr`](mailto:peio.borthelle@univ-smb.fr)
|
||||
|
||||
Github
|
||||
: [`@lapin0t`](https://github.com/lapin0t/)
|
||||
|
||||
SourceHut
|
||||
: [`~lapinot`](https://sr.ht/~lapinot/)
|
||||
|
||||
ORCID
|
||||
: [`0009-0006-7733-7439`](https://orcid.org/0009-0006-7733-7439)
|
||||
|
||||
|
||||
## Events {: #events }
|
||||
|
||||
- Will present at [GALOP'24](https://popl24.sigplan.org/home/galop-2024) (London, UK)
|
||||
"An abstract, certified account of Operational Game Semantics".
|
||||
- Presented at [TYPES'23](https://types2023.webs.upv.es/) (Valencia, Spain) a
|
||||
short introduction on using a spin-off of polynomial functors to describe
|
||||
games
|
||||
([slides](https://types2023.webs.upv.es/slides/S12/TYPES2023-borthelle-Hirshowitz-Jaber-Zakowski.pdf)
|
||||
and [talk
|
||||
recording](https://media.upv.es/#/portal/video/a41afdb0-33ba-11ee-8317-3dc1d7f6252c)).
|
||||
- Attended [AIMXXXVI](https://wiki.portal.chalmers.se/agda/Main/AIMXXXVI) (Delft, Netherlands).
|
||||
- Attended
|
||||
[OPLSS'22](https://www.cs.uoregon.edu/research/summerschool/summer22/)
|
||||
(Eugene, Oregon, USA).
|
||||
|
||||
## Research Interests {: #interests }
|
||||
|
||||
The main topic of my thesis (as of january 2024!) is to investigate the
|
||||
formalization of a particular kind of game (or trace) semantics based on
|
||||
automatons: operational game semantics.
|
||||
|
||||
I am broadly interested in programming languages (all kinds), type theory,
|
||||
dependently typed programming, interactive semantics (games and co). However
|
||||
this list is both too broad and too restrictive, so I will rather list
|
||||
a couple papers I recently liked (in no particular order):
|
||||
|
||||
- *Compiling with Classical Connectives*, Paul Downen and Zena M. Ariola,
|
||||
LMCS 2020. A very clear introduction to the mu-mu-tilde language. Pretty
|
||||
mind-blowing for who has been convinced that classical logic has no
|
||||
computational content.
|
||||
- Both *A type- and scope-safe universe of syntaxes with binding: their
|
||||
semantics and proofs*, Guillaume Allais, Robert Atkey, James Chapman, Conor
|
||||
McBride and James McKinna, JFP 2021 and *Formal metatheory of second-order
|
||||
abstract syntax*, Marcelo Fiore and Dmitrij Szamozvancev, POPL 2022. Both
|
||||
papers present the now standard approach for formalizing simply-typed
|
||||
languages in type theory, both in literate Agda. The first is perhaps more
|
||||
oriented towards the dependently-typed programmer and the second towards the
|
||||
category-enclined computer scientist. See also on this topic the [excellent
|
||||
tutorial](https://gitlab.inria.fr/fpottier/mpri-2.4-public/-/blob/master/agda/02-dependent/Indexed.lagda.rst)
|
||||
by Pierre-Evariste Dagand.
|
||||
- *Normalization by Evaluation for Call-by-Push-Value and Polarized
|
||||
Lambda-Calculus*, Andreas Abel and Christian Sattler, PPDP 2019. Section 2
|
||||
alone is worth the read and develops an Agda formalization of NBE for a
|
||||
simply typed lambda-calculus *with positive connectives* (here sums). Until
|
||||
this paper I didn't realize that the go-to minimal example of STLC with
|
||||
products has only *negative types*. In fact quite a big (but elegant) fix is
|
||||
needed to deal with positives.
|
||||
- The two very cute complete lattice papers *Coinduction All the Way Up*,
|
||||
Damien Pous, LICS 2016 and *Tower Induction and Up-To Techniques for CCS with
|
||||
Fixed Points*, Steven Schäfer and Gert Smolka, RAMICS 2017, both of which are
|
||||
implemented in Damien's Coq library
|
||||
[`coq-coinduction`](https://github.com/damien-pous/coinduction). I believe
|
||||
they form a line of follow-ups on the two (generalized) parametrized
|
||||
coinduction papers by Chung-Kil Hur et al., which first introduced a similar
|
||||
library, [`paco`](https://github.com/snu-sf/paco). They introduce easily
|
||||
described but very powerful gadgets for dealing with exotic coinductive
|
||||
reasoning schemes.
|
||||
- *Substitution, jumps, and algebraic effects*, Marcelo Fiore and Sam Staton,
|
||||
LICS 2014. A neat development on a sort of generic effect which can be read
|
||||
as a high-level presentation of a low level implementation technique.
|
||||
- *A Linear Algebra Approach to Linear Metatheory*, James Wood and Bob Atkey,
|
||||
TLLA 2020. A particularly compelling attempt at cracking the nut of an
|
||||
approachable intrinsically typed and scoped syntax for substructural calculi.
|
||||
|
||||
## Publications {: #pubs }
|
||||
|
||||
For now this list is pretty empty, a couple things are currently cooking, come
|
||||
back later!
|
||||
|
||||
- *A Cellular Howe Theorem*, Peio Borthelle, Tom Hirschowitz and Ambroise
|
||||
Lafont, LICS 2020, ([pdf](https://hal.science/hal-02880876v1/file/main.pdf),
|
||||
[doi](https://doi.org/10.1145/3373718.3394738)). The writeup of work I did during
|
||||
my masters internship with Tom, which he continued with Ambroise (they further wrote
|
||||
two follow-ups, covering more instances of Howe's method).
|
||||
Loading…
Reference in New Issue