Add ReFL x Crystal meeting, update members
This commit is contained in:
parent
ce940a45dd
commit
ca052acc02
|
|
@ -1,2 +1,3 @@
|
|||
public/
|
||||
resources/
|
||||
hugo
|
||||
|
|
|
|||
|
|
@ -4,8 +4,12 @@ title: "Meetings"
|
|||
|
||||
Some meetings were private and informal. For these reasons, they are not recorded here.
|
||||
|
||||
- **"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](/ri2025/)
|
||||
- **"Introduction to transcendental syntax"** (June 20th, 2024) by Boris Eng and Pablo Donato (5 people).
|
||||
- **"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).
|
||||
|
|
|
|||
|
|
@ -6,16 +6,21 @@ title: "Members"
|
|||
|
||||
- [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 🌸](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/) (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://www.engboris.fr) (administrator, coordinator)<div class="desc-box">Transcendental syntax, computer science -- OCamlPro (private company)</div>
|
||||
- [Boris Eng 🦖](https://www.engboris.fr) (administrator, coordinator)<div class="desc-box">Transcendental syntax, proof theory, linear logic -- OCamlPro (private company)</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
|
||||
|
||||
- [Léo Andrès](https://www.zapashcanon.fr/)<div class="desc-box"> compilation, functional programming, symbolic execution, programming languages -- OCamlPro (private company)</div>
|
||||
- Victor Benitah
|
||||
- [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 (Galinette)</div>
|
||||
- [Charles Grellois](https://www.sheffield.ac.uk/cs/people/academic/charles-grellois)<div class="desc-box">University of Sheffield</div>
|
||||
- [Xavier Denis](https://xav.io/)<div class="desc-box">Deductive verification and specification of Rust programs</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<div class="desc-box">Logic, LLM (Machine learning) -- Université Paris Cité (IRIF)</div>
|
||||
|
|
@ -23,8 +28,12 @@ title: "Members"
|
|||
- 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>
|
||||
- [Tito](https://nguyentito.eu/)<div class="desc-box">Links between linear logic and automata theory, combinatorics, computational complexity, algorithms -- CNRS & Aix-Marseille</div>
|
||||
- [Xavier Denis](https://xav.io/)<div class="desc-box">Deductive verification and specification of Rust programs -- ETH Zurich</div>
|
||||
|
||||
# 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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
<div class="desc-box">Participants: Boris Eng.</div>
|
||||
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
|
||||
|
||||
<div class="desc-box">Participants: Boris Eng.</div>
|
||||
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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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`.
|
||||
24
hugo.toml
24
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"
|
||||
|
|
|
|||
|
|
@ -6,4 +6,4 @@
|
|||
gtag('js', new Date());
|
||||
|
||||
gtag('config', 'G-7308Y1HGM9');
|
||||
</script>
|
||||
</script>
|
||||
|
|
|
|||
Loading…
Reference in New Issue