Merge remote history before migration

.gitignore

@@ -1,31 +1,3 @@
-# build output
+public/
-dist/
+resources/
-
+hugo
-# generated types
-.astro/
-
-# dependencies
-node_modules/
-playwright-report/
-test-results/
-
-# logs
-npm-debug.log*
-yarn-debug.log*
-yarn-error.log*
-pnpm-debug.log*
-
-# environment variables
-.env
-.env.production
-
-# macOS-specific files
-.DS_Store
-
-# jetbrains setting folder
-.idea/
-
-# obsidian workspace settings
-.obsidian/
-
-.vscode/

archetypes/default.md

@@ -0,0 +1,5 @@
++++
+title = '{{ replace .File.ContentBaseName "-" " " | title }}'
+date = {{ .Date }}
+draft = true
++++

content/_index.md

@@ -0,0 +1,52 @@
+---
+paige:
+  search:
+    hide_page: true
+  style: |
+    #paige-collections,
+    #paige-metadata,
+    #paige-sections,
+    #paige-pages {
+        display: none;
+    }
+    #paige-title {
+        font-size: 5rem;
+    }
+title: "ReFL"
+---
+
+<!-- {{% paige/image alt="Landscape" breakpoints=true class="object-fit-cover rounded-4 shadow-lg" fetchpriority="high" height="20rem" loading="eager" process="webp" src="https://images.unsplash.com/photo-1490604001847-b712b0c2f967?w=1296" width="100%" %}}
+
+<br /><br /> -->
+
+French scientific network on the foundations of logic and computation. The group was initially founded by four PhD students during the “Linear Logic Winter School 2022” but we now aim for a broader group where discussions can be initiated between logicians, computer scientists, mathematicians, philosophers and more. We have people with various backgrounds and profiles and we all share a taste for deep questions and the aim of proposing original insights and new perspectives of the foundations of computation and logic. In particular, we take a great interest in the role of computer science in the understanding of logic.
+
+We are inspired by the transdisciplinarity of the LIGC working group which gathered researchers from various fields around the foundations of (linear) logic.
+
+We use French for our discussions, seminars and meetings but we are open to English speakers for discussions.
+
+Our Zulip chat: [chat.refl.fr](http://chat.refl.fr)
+
+Our mailing list: `refl@framalistes.org`
+
+**Our scientific interests**
+
+- foundations and philosophy of logic, computation and mathematics
+- history of logic and computation
+- category theory and its applications
+- proof-program correspondence and proof/type theory
+- Jean-Yves Girard's works: linear logic, proof-nets, ludics, geometry of interaction, transcendental syntax
+
+**Our activities**
+
+- seminars (generally online)
+- debates and discussions on Zulip
+- private meetings in person between some participants
+- collaboration and mutual assistance (thesis, research, software, programming, ...)
+- writing, communication, programming projects
+
+# Sponsors
+
+<br />
+<p style="font-size: 18px;"><a style="margin-right: 20px;" href="https://zulip.com/"><img src="/images/zulip.png"></a>
+Sponsored by Zulip. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.</p>

content/meetings.md

@@ -0,0 +1,42 @@
+---
+title: "Meetings"
+---
+
+Some meetings were private and informal. For these reasons, they are not recorded here.
+
+- **"Meeting around Jean-Yves Girard"** (Nov 23th, 2025) (4 people).
+- **"Meeting RI2025 in Morbihan"** (April 28th -- May 2nd, 2025) organised by Jérémy Hervé, Boris Eng, Victor Benitah (around 16 people).
+    + [Details of the meeting](/refli2025/)
+- **"Fondements esthétiques de la logique"** (November 1st, 2024) by Pierre Cardascia (16 people).
+	+ ["Morts du mythe, de l’art, de la philosophie, de la logique : Itinéraire d’un problème serial-killer"](/documents/cardascia-01-11-2024.pdf), Pierre Cardascia (1h30)
+- **"Introduction to transcendental syntax"** (June 20th, 2024) by Boris Eng and Pablo Donato (5 people).
+- **"Analytic and continental philosophy"** (May 20th, 2024) by Luc Pommeret (17 people).
+	+ "Le professionnel et l'écrivain : le pouvoir offensif de la philosophie analytique", Luc Pommeret (1h30)
+- **"Technical introduction to transcendental syntax"** (May 11th, 2024) (4 people).
+	+ "Introduction to Peirce's philosophy", Pablo Donato (30min).
+	+ "Stellar resolution and Girard's knitting", Boris Eng.
+- **"Meeting around Jean-Yves Girard"** (May 10th, 2024) (5 people).
+- **"Program verification"** (June 26th, 2023) by Xavier Denis.
+	+ "Presentation of the Rust programming language", Xavier Denis (1h)
+	+ "Why formal verification is getting it wrong", Xavier Denis (1h)
+- **"Logic and quantum computation"** (May 31th, 2023) by Kostia Chardonnet. Chair: Kostia Chardonnet.
+	+ "Quantum computation and Geometry of Interaction", Kostia Chardonnet (45min)
+- **"Logic and Categories"** (March 24th, 2023) by Tito and Valentin Maestracci. Chair: Pablo Donato.
+	+ ["Pourquoi les catégories sont la bonne façon de faire de la sémantique dénotationnelle"](https://nguyentito.eu/2023-03-refl.pdf), Tito (1h)
+	+ "Catégories monoïdales à trace", Valentin Maestracci (1h)
+- **"ReFL first seminar of the year"** (February 21, 2023) by Pablo Donato, Davide Barbarossa, Adrien Ragot, Boris Eng, Sidney Congard (around 13 people online). Chair: Boris Eng.
+	+ "Du calcul des séquents à la logique linéaire", Pablo Donato (30min)
+	+ "Correspondance de Curry-Howard et théorie des types", Davide Barbarossa (30min)
+	+ "Réseaux de preuve multiplicatifs avec règle daemon", Adrien Ragot (30min)
+	+ ["Introduction à la géométrie de l'interaction originale de Girard"](https://engboris.fr/documents/slides_tc1_2023.pdf), Boris Eng (30min)
+	+ "Introduction à la syntaxe transcendantale", Sidney Congard (30min)
+- **"Freedom and Control in Logic and Computation"** (February 1st, 2023) (4 people).
+	+ Apodictic and Epidictic in Girard's transcendental syntax. Control over computation (synchronicity, sequentiality, direction of computation).
+- **"Proof-nets and Deep Inference"** (April 27, 2022) by Pablo Donato (5 people).
+	+ Comparison between deep inference and proof-nets. Non-sequentialisable multiplicative connectives, ludics, proof assistants, sequent calculi as recipes for computational objects (constellations).
+- **"Computation and Meaning"** (March 23, 2022) by Boris Eng (8 people).
+	+ Discussion on stellar resolution and ways to put meaning on it (Girard's "usine" and "usage"), correctness criterion, realisability theory.
+- **"Lambda-calculus and stellar resolution"** (March 9, 2022) by Boris Eng and Julien Marquet (6 people).
+	+ Discussion on possible encodings of lambda-calculus and Lafont's interaction nets with unification (by using stellar resolution). Decomposition of tests as constellations. Discussions on optimal reduction of lambda-calculus.
+- **Round table discussion at CIRM's "Logic and Interaction"** thematic month (February 2022) (8 people).
+	+ Discussions on Girard's transcendental syntax. Focus on Girard's "conceptual knitting".

content/members.md

@@ -0,0 +1,39 @@
+---
+title: "Members"
+---
+
+# Co-founders
+
+- [Davide Barbarossa](https://davidebarbarossa12.github.io/index.html)<div class="desc-box">Lambda-calculus, type theory, linear logic, category theory, classical realizability, philosophy of mathematics -- Università di Bologna</div>
+- [Pablo Donato 🌸](https://pablogician.refl.fr/) (administrator)<div class="desc-box">proof theory, type theory, topos theory, proof assistants, human-computer interaction, end-user programming -- Grothendieck Institute</div>
+- [Boris Eng 🦖](https://engboris.refl.fr) (administrator, coordinator)<div class="desc-box">Transcendental syntax, proof theory, linear logic -- R&D engineer at OCamlPro</div>
+- [Valentin Maestracci](https://vmaestracci.github.io/)<div class="desc-box">Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille</a>
+
+# Members
+
+- Victor Benitah<div class="desc-box"> formal systems explorer, co-founder of an electronic firm -- Airline pilot at Air France</div>
+- [Hugo Cadière](https://www.univ-lyon3.fr/m-hugo-cadiere)<div class="desc-box"> Philosophy of mathematics / computer Science / language / mind, German Idealism and XXth century German philosohy -- Université Jean-Moulin Lyon 3</div>
+- [Pierre Cardascia 🎲](https://suboptimal.games/)<div class="desc-box">Philosophy, Game Design, Entrepreneurship, Immersive Experience, Poetry -- SubOptimal Games (private company)</div>
+- Baptiste Chanus<div class="desc-box">Descriptive complexity -- Université Paris 1 Panthéon-Sorbonne</div>
+- [Kostia Chardonnet](https://kostiachardonnet.github.io/)<div class="desc-box">Computer science, quantum computation, cyclic proofs -- Centre Inria de l'Université de Lorraine (MOCQUA)</div>
+- [Sidney Congard](https://dwarfobserver.github.io/)<div class="desc-box">Semantics of programming languages -- Centre Inria de l'Université de Rennes (Gallinette)</div>
+- [Xavier Denis](https://xav.io/)<div class="desc-box">Deductive verification and specification of Rust programs</div>
+- Pierre Benjamin Giraud<div class="desc-box">Multi-dimensional (Logic ⊗ (Cubes & Rewriting systems) ⊗ Automata), automata for proofs, philoTechny of mathematics -- Centre Inria de l'Université de Rennes (Gallinette)</div>
+- [Charles Grellois](https://www.sheffield.ac.uk/cs/people/academic/charles-grellois)<div class="desc-box">
+  Semantics, (linear) logic, automata theory, higher-order model-checking, mathematical modeling, probabilistic termination, algebra/categories to model real-world problems - University of Sheffield</div>
+- Jérémy Hervé 🍄<div class="desc-box">Mushrooms, operating systems design -- Independent</div>
+- [Ambroise Lafont](https://amblafont.github.io/)<div class="desc-box">Type Theory and Category Theory -- École Polytechnique (LIX)</div>
+- [Luc Pommeret](https://lucpommeret.com/)<div class="desc-box">Logic, LLM (Machine learning) -- Laboratoire Interdisciplinaire des Sciences du Numérique de Paris-Saclay (LISN)</div>
+- Adrien Ragot<div class="desc-box">Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic -- Université Sorbonne Paris Nord / University Roma Tre</div>
+- Paul Séjourné<div class="desc-box">Archaic and contemporary philosophy (of mathematics), algebraic geometry, category theory -- Université Paris-Sorbonne</div>
+- [Vincent Moreau](https://www.irif.fr/~moreau/)<div class="desc-box">Category theory, type theory, denotational semantics, topology, algebra, proof assistants -- Université Paris Cité (IRIF)</div>
+- François-René Rideau (Faré)
+- [Tito](https://nguyentito.eu/)<div class="desc-box">Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- CNRS & Aix-Marseille</div>
+
+# Visitors and guests
+
+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, Roman Perez, Nico, Chirine
+Laghjichi, Jonty Male, Alexis Toumi, Baptiste Colin.

content/refli2025.md

@@ -0,0 +1,38 @@
+---
+title: "ReFLi 2025 Meeting"
+---
+
+Rencontre du **28 avril 2025** au **2 mai 2025** à Lizio (Morbihan).
+
+**Organisateurs :**
+- Victor Benitah;
+- Boris Eng;
+- Jérémy Hervé.
+
+La rencontre est organisée par l'association _"Reflets Intemporels"_ fondée
+pour l'occasion.
+
+Il s'agit d'une rencontre réunissant environ 16 personnes. Parmi ces
+participants, des membres et proches du réseau de recherche _ReFL_ et de la
+société privée 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 d'échanges cadrés et quelques exposés
+très courts.
+
+La rencontre tournera autour des grands thèmes de la **vérité**, de la
+**fiabilité** et de la notion de **système**, teinté d'ingénierie mais sans y
+être limité.
+
+**Autres sujets d'intérêt des participants :**
+- fondements de la logique et des mathématiques;
+- epistémologie;
+- cybernétique et systèmes complexes;
+- musique;
+- enseignement;
+- électronique;
+- conception des langages de programmation et des systèmes d'exploitation;
+- fiabilité des systèmes;
+- décentralisation (internet, blockchains, ...).

content/resources.md

@@ -0,0 +1,16 @@
+---
+title: "Resources"
+---
+
+- *"Le fantôme de la transparence"* -- Jean-Yves Girard
+- [*Syntaxe transcendentale (Wikipédia)*](https://fr.wikipedia.org/wiki/Syntaxe_transcendantale)
+- [*Transcendental Syntax (nlab)*](https://ncatlab.org/nlab/show/transcendental+syntax)
+- [*"An exegesis of transcendental syntax" (PhD thesis)* -- Boris Eng](https://hal.science/tel-04179276v1)
+- [*"La logique face à l'arbitraire" (French)* -- Sidney Congard](https://hal.science/hal-03689001/document)
+- [*"Les limites de la correspondance preuve/programme" (French)* -- Laurent Regnier](https://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/ch.pdf)
+- [*"Aristote et l’électricien : le branchement des idées" (French video)* -- Paolo Pistone](https://vimeo.com/167115532)
+- [*"D'une logique à l'autre" (French video)* -- Laurent Regnier](https://vimeo.com/314743657)
+- [*"Symmetry and interactivity in Programming"* -- Pierre-Louis Curien](https://hal.archives-ouvertes.fr/hal-00003868/)
+- [*"Radical anti-realism and substructural logics"* -- Jacques Dubucs & Mathieu Marion](https://halshs.archives-ouvertes.fr/halshs-00000055/)
+- [*"Which Logic for the Radical Anti-Realist?"* -- Denis Bonnay & Mikaël Cozic](https://halshs.archives-ouvertes.fr/halshs-00775655)
+- [*"Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic" -- Paolo Pistone*](https://hal.archives-ouvertes.fr/hal-01309218)

go.mod

@@ -0,0 +1,5 @@
+module git.epidictic.fr/ReFL/www-refl-fr
+
+go 1.18
+
+require github.com/willfaught/paige v0.75.0 // indirect

go.sum

@@ -0,0 +1,2 @@
+github.com/willfaught/paige v0.75.0 h1:ZwneL6YjYif4MQ6ROnbiQX9apY5hXoplsVPPt3kTgRI=
+github.com/willfaught/paige v0.75.0/go.mod h1:0Nt8ifl7UVYQIBaMtpZmg+BrQHHzFNqKcrBoA2Oo4/E=

hugo.toml

@@ -0,0 +1,70 @@
+baseurl = "https://refl.fr"
+copyright = "© ReFL, website based on Will Fraught's Paige theme for Hugo"
+enablerobotstxt = true
+languagecode = "en-us"
+timezone = "Europe/Paris"
+titlecasestyle = "Go"
+
+[languages.en]
+title = "ReFL"
+weight = 10
+
+[[languages.en.menu.main]]
+identifier = "home"
+name = "Home"
+url = "/"
+weight = 10
+
+[[languages.en.menu.main]]
+identifier = "members"
+name = "Members"
+url = "/members/"
+weight = 20
+
+[[languages.en.menu.main]]
+identifier = "meetings"
+name = "Meetings"
+url = "/meetings/"
+weight = 40
+
+[[languages.en.menu.main]]
+identifier = "resources"
+name = "Resources"
+url = "/resources/"
+weight = 50
+
+[markup.goldmark.renderer]
+unsafe = true
+
+[markup.highlight]
+noclasses = false
+
+[markup.tableofcontents]
+endlevel = 6
+ordered = true
+startlevel = 2
+
+[[module.imports]]
+path = "github.com/willfaught/paige"
+
+[params.authors.will-faught]
+default = true
+email = "will.faught@example.com"
+name = "Will Faught"
+url = "https://willfaught.com/paige"
+
+[params.paige]
+site_title = "ReFL"
+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.rss]
+managing_editor = "will.faught@example.com (Will Faught)"
+web_master = "will.faught@example.com (Will Faught)"
+
+[params.paige.file_link]
+content = "Edit this page"
+disable = true
+url = "https://github.com/willfaught/paige/edit/master/exampleSite/content/%s"

layouts/home.html

@@ -0,0 +1,7 @@
+{{ define "main" }}
+{{ $page := . }}
+
+{{ partial "paige/article.html" $page }}
+{{ partial "paige/pages.html" $page }}
+
+{{ end }}

layouts/partials/paige/footer-first.html

@@ -0,0 +1 @@
+<br />

layouts/partials/paige/head-first.html

@@ -0,0 +1,9 @@
+<!-- Google tag (gtag.js) -->
+<script async src="https://www.googletagmanager.com/gtag/js?id=G-7308Y1HGM9"></script>
+<script>
+  window.dataLayer = window.dataLayer || [];
+  function gtag(){dataLayer.push(arguments);}
+  gtag('js', new Date());
+
+  gtag('config', 'G-7308Y1HGM9');
+</script>

layouts/partials/paige/main-first.html

@@ -0,0 +1 @@
+<hr />

layouts/partials/paige/style-first.css

@@ -0,0 +1,49 @@
+#paige-authors,
+#paige-breadcrumbs,
+#paige-credit,
+#paige-date,
+#paige-keywords,
+#paige-reading-time,
+#paige-series,
+#paige-toc,
+.paige-authors,
+.paige-date,
+.paige-date-header,
+.paige-keywords,
+.paige-reading-time,
+.paige-series,
+.paige-summary {
+    display: none;
+}
+
+#paige-content {
+    font-size: 1.25rem;
+    font-weight: 300;
+}
+
+b, strong {
+    font-weight: bold;
+}
+
+hr {
+    opacity: 0.15;
+}
+
+.desc-box {
+    font-size: 16px;
+    color: rgb(120, 120, 120);
+}
+
+a {
+    font-weight: bolder;
+    text-decoration: none;
+    color: rgb(40, 173, 145);
+}
+
+a:hover {
+    opacity: 0.5;
+}
+
+.nav-link {
+    color: rgb(40, 173, 145);
+}