commit bf34e8e67673fe490032abd10dfd3fbf30a4ae2f Author: lapinot Date: Thu Jan 4 12:49:18 2024 +0100 initial commit diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..8de56d8 --- /dev/null +++ b/Makefile @@ -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 diff --git a/src/assets/theme.css b/src/assets/theme.css new file mode 100644 index 0000000..a0142b1 --- /dev/null +++ b/src/assets/theme.css @@ -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; +} diff --git a/src/build.py b/src/build.py new file mode 100644 index 0000000..f5e8444 --- /dev/null +++ b/src/build.py @@ -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)) diff --git a/src/index.html b/src/index.html new file mode 100644 index 0000000..0013457 --- /dev/null +++ b/src/index.html @@ -0,0 +1,28 @@ + + + + + Peio Borthelle + + + + + + + + + +
+ {{ content }} +
+
+ + + diff --git a/src/index.md b/src/index.md new file mode 100644 index 0000000..bdb3137 --- /dev/null +++ b/src/index.md @@ -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).