Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics -- Università di Bologna
- [Pablo Donato 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (administrator)proof theory, type theory, topos theory, proof assistants, human-computer interaction, end-user programming -- Grothendieck Institute
-- [Boris Eng 🦖](https://www.engboris.fr) (administrator, coordinator)Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille
# Members
+- [Léo Andrès](https://www.zapashcanon.fr/)
compilation, functional programming, symbolic execution, programming languages -- OCamlPro (private company)
+- Victor Benitah
+- [Hugo Cadière](https://www.univ-lyon3.fr/m-hugo-cadiere)
Philosophy of mathematics / computer Science / language / mind, German Idealism and XXth century German philosohy -- Université Jean-Moulin Lyon 3
- [Pierre Cardascia 🎲](https://suboptimal.games/)
Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry -- SubOptimal Games (private company)
- Baptiste Chanus
Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne
- [Kostia Chardonnet](https://kostiachardonnet.github.io/)
Computer science, quantum computation, cyclic proofs -- Centre Inria de l'Université de Lorraine (MOCQUA)
- [Sidney Congard](https://dwarfobserver.github.io/)
Semantics of programming languages -- Centre Inria de l'Université de Rennes (Galinette)
-- [Charles Grellois](https://www.sheffield.ac.uk/cs/people/academic/charles-grellois)
University of Sheffield
+- [Xavier Denis](https://xav.io/)
Deductive verification and specification of Rust programs
+- [Charles Grellois](https://www.sheffield.ac.uk/cs/people/academic/charles-grellois)
+ Semantics, (linear) logic, automata theory, higher-order model-checking, mathematical modeling, probabilistic termination, algebra/categories to model real-world problems - University of Sheffield
- Jérémy Hervé 🍄
Mushrooms, operating systems design -- Independent
- [Ambroise Lafont](https://amblafont.github.io/)
Type Theory and Category Theory -- École Polytechnique (LIX)
- Luc Pommeret
Logic, LLM (Machine learning) -- Université Paris Cité (IRIF)
@@ -23,8 +28,12 @@ title: "Members"
- Paul Séjourné
Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory -- Université Paris-Sorbonne
- [Vincent Moreau](https://www.irif.fr/~moreau/)
Category theory, type theory, denotational semantics, topology, algebra, proof assistants -- Université Paris Cité (IRIF)
- [Tito](https://nguyentito.eu/)
Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- CNRS & Aix-Marseille
-- [Xavier Denis](https://xav.io/)
Deductive verification and specification of Rust programs -- ETH Zurich
# Visitors and guests
-Hugo Cadière, Titouan Carette, Clémence Chanavat, Bernardo Marques, Julien Marquet, Rémi Nollet, Federico Olimpieri, Raphael Tossings, Pierre Vial, Quentin, Gael Deest, Martin Tricaud, Fadi Shawki, Eliès Harington, Axel Kerinec, Aloÿs Dufour, Bernardo, Anne-Laure, Escherichia, Alexey, François-René Rideau (Faré), Roman Perez, Nico.
+Titouan Carette, Clémence Chanavat, Bernardo Marques, Julien Marquet, Rémi
+Nollet, Federico Olimpieri, Raphael Tossings, Pierre Vial, Quentin, Gael Deest,
+Martin Tricaud, Fadi Shawki, Eliès Harington, Axel Kerinec, Aloÿs Dufour,
+Bernardo, Anne-Laure, Escherichia, Alexey, François-René Rideau (Faré), Roman
+Perez, Nico, Chirine Laghjichi, Jonty Male, Alexis Toumi, Baptiste Colin,
+Pierre Giraud.
diff --git a/content/projects.md b/content/projects.md
index 656f270..651a444 100644
--- a/content/projects.md
+++ b/content/projects.md
@@ -4,34 +4,32 @@ title: "Projects"
# Reading
-## >> Normalisation by Evaluation (NbE)
-
-Participants: Vincent Moreau, Ambroise Lafont, Tito, Valentin Maestracci,
-Sidney Congard.
-
## >> Wittgenstein's "De la certitude"
Participants: Vincent Moreau, Tito, Boris Eng, Sidney Congard.
# Development of Girard's Transcendental Syntax
-## >> A programming guide to transcendental syntax
+## >> Development of the Stellogen programming language
Participants: Boris Eng.
-The goal is to develop a programming guide (in the idea of Software Foundations
-for Coq) in order to make the ideas of Girard's transcendental syntax more
-accessible. Eng's implementation of stellar resolution, named LSC (Large Star
-Collider) will be used for that purpose. Exercises (with solutions) have to be
-designed to open the development of transcendental syntax to contributions.
+Stellogen is a minimalistic and logic-agnostic programming language based on
+term unification. The goal is to develop a programming language and a guide
+(in the idea of Software Foundations for Coq) in order to make the ideas of
+Girard's transcendental syntax more accessible. Exercises (with solutions) have
+to be designed to open the development of transcendental syntax to
+contributions.
-[https://tsguide.refl.fr](https://tsguide.refl.fr)
+- [https://tsguide.refl.fr](https://tsguide.refl.fr)
+- [https://tsguide.refl.fr](https://tsguide.refl.fr)
+- [https://tsguide.refl.fr/en](https://tsguide.refl.fr/en)
## >> A new manifest for transcendental syntax
Participants: Boris Eng.
Writing of a roadmap for transcendental syntax with an analysis of various
fields of logic and computation and several links with other fields. The point
-is to show that transcendental syntax is actually a rich subject.
+is to show that transcendental syntax is actually a big project.
## >> Tunes OS: a reflexive operating system
@@ -52,3 +50,9 @@ Séjourné.
## >> Reading and comments on Krivine's "Les décompilateurs"
By Boris Eng.
+
+## >> Normalisation by Evaluation (NbE)
+
+Participants: Vincent Moreau, Ambroise Lafont, Tito, Valentin Maestracci,
+Sidney Congard.
+
diff --git a/content/refli2025.md b/content/refli2025.md
new file mode 100644
index 0000000..76c595d
--- /dev/null
+++ b/content/refli2025.md
@@ -0,0 +1,36 @@
+---
+title: "ReFLi 2025 Meeting"
+---
+
+Rencontre du **28 avril 2025** au **2 mai 2025** au Morbihan.
+
+**Organisateurs :**
+- Victor Benitah;
+- Boris Eng;
+- Jérémy Hervé.
+
+Le séminaire est organisé par l'association _"Reflets Intemporels"_ fondée dans
+le cadre de cette rencontre.
+
+Il s'agit d'une rencontre réunissant environ 16 personnes provenant du réseau
+de recherche _ReFL_ et de la société privée (et proches) d'électronique
+_Crystal_.
+
+Cette rencontre est l'occasion d'exprimenter à la fois les capacités de ReFL et
+Crystal à organiser et des rencontres scientifiques mais aussi d'explorer des
+méthodes différentes de communication et de collaboration. Les suggestions
+d'activités comprennent : des sessions focalisées sur des échanges plus locaux
+(par petits groupes aléatoires et dynamiques) pouvant inclure ou non une
+collaboration locale sur des problématiques données, limitation (mais
+conservation) de présentations "unidirectionnelles".
+
+**Thèmes d'intérêt :**
+- fondements de la logique et des mathématiques;
+- cybernétique et systèmes complexes;
+- électronique;
+- conception des langages de programmation et des systèmes d'exploitation;
+- fiabilité des systèmes;
+- décentralisation (internet, blockchains, ...).
+
+Pour plus d'information sur comment se rendre sur place ou en cas de problème
+veuillez contacter votre référent. Sinon, contacter `boris.eng@proton.me`.
diff --git a/hugo.toml b/hugo.toml
index 90a9353..2618aac 100644
--- a/hugo.toml
+++ b/hugo.toml
@@ -2,7 +2,6 @@ baseurl = "https://refl.fr"
copyright = "© ReFL, website based on Will Fraught's Paige theme for Hugo"
enablerobotstxt = true
languagecode = "en-us"
-paginate = 50
timezone = "Europe/Paris"
titlecasestyle = "Go"
@@ -28,6 +27,12 @@ name = "Projects"
url = "/projects/"
weight = 30
+[[languages.en.menu.main]]
+identifier = "refli2025"
+name = "ReFLi 2025 Meeting"
+url = "/refli2025/"
+weight = 35
+
[[languages.en.menu.main]]
identifier = "meetings"
name = "Meetings"
@@ -54,12 +59,6 @@ startlevel = 2
[[module.imports]]
path = "github.com/willfaught/paige"
-[outputs]
-home = ["atom", "html", "paige-search", "rss"]
-section = ["atom", "html", "rss"]
-taxonomy = ["atom", "html", "rss"]
-term = ["atom", "html", "rss"]
-
[params.authors.will-faught]
default = true
email = "will.faught@example.com"
@@ -73,11 +72,6 @@ site_description = "Réflexions sur les Fondements de la Logique"
[params.paige.git]
commit_url = "https://github.com/willfaught/paige/commit/%s"
-[[params.paige.feed.atom.authors]]
-email = "will.faught@example.com"
-name = "Will Faught"
-url = "https://willfaught.com/paige"
-
[params.paige.feed.rss]
managing_editor = "will.faught@example.com (Will Faught)"
web_master = "will.faught@example.com (Will Faught)"
@@ -86,9 +80,3 @@ web_master = "will.faught@example.com (Will Faught)"
content = "Edit this page"
disable = true
url = "https://github.com/willfaught/paige/edit/master/exampleSite/content/%s"
-
-[taxonomies]
-author = "authors"
-category = "categories"
-series = "series"
-tag = "tags"
diff --git a/layouts/partials/paige/head-first.html b/layouts/partials/paige/head-first.html
index b5e79fa..31a5826 100644
--- a/layouts/partials/paige/head-first.html
+++ b/layouts/partials/paige/head-first.html
@@ -6,4 +6,4 @@
gtag('js', new Date());
gtag('config', 'G-7308Y1HGM9');
-
\ No newline at end of file
+