From 793ecb7b7772924b8af8b05cb5b491a6e3c6f951 Mon Sep 17 00:00:00 2001 From: engboris Date: Wed, 1 May 2024 21:48:20 +0200 Subject: [PATCH] Add first version of the website --- .gitignore | 2 + archetypes/default.md | 5 ++ content/_index.md | 48 ++++++++++++ content/meetings.md | 25 ++++++ content/members.md | 28 +++++++ content/projects.md | 5 ++ content/resources.md | 13 ++++ go.mod | 5 ++ go.sum | 2 + hugo.toml | 94 +++++++++++++++++++++++ layouts/home.html | 7 ++ layouts/partials/paige/footer-first.html | 1 + layouts/partials/paige/main-first.html | 1 + layouts/partials/paige/style-first.css | 45 +++++++++++ static/images/zulip.png | Bin 0 -> 3237 bytes 15 files changed, 281 insertions(+) create mode 100644 .gitignore create mode 100644 archetypes/default.md create mode 100644 content/_index.md create mode 100644 content/meetings.md create mode 100644 content/members.md create mode 100644 content/projects.md create mode 100644 content/resources.md create mode 100644 go.mod create mode 100644 go.sum create mode 100644 hugo.toml create mode 100644 layouts/home.html create mode 100644 layouts/partials/paige/footer-first.html create mode 100644 layouts/partials/paige/main-first.html create mode 100644 layouts/partials/paige/style-first.css create mode 100644 static/images/zulip.png diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..73ab876 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +public/ +resources/ diff --git a/archetypes/default.md b/archetypes/default.md new file mode 100644 index 0000000..c6f3fce --- /dev/null +++ b/archetypes/default.md @@ -0,0 +1,5 @@ ++++ +title = '{{ replace .File.ContentBaseName "-" " " | title }}' +date = {{ .Date }} +draft = true ++++ diff --git a/content/_index.md b/content/_index.md new file mode 100644 index 0000000..c1e873c --- /dev/null +++ b/content/_index.md @@ -0,0 +1,48 @@ +--- +paige: + search: + hide_page: true + style: | + #paige-collections, + #paige-metadata, + #paige-sections, + #paige-pages { + display: none; + } + #paige-title { + font-size: 5rem; + } +--- + + + +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 relectures 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 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 + +# Sponsors + +

+Sponsored by Zulip. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.

\ No newline at end of file diff --git a/content/meetings.md b/content/meetings.md new file mode 100644 index 0000000..243f8a7 --- /dev/null +++ b/content/meetings.md @@ -0,0 +1,25 @@ +--- +title: "Meetings" +--- + +Some meetings were private and informal. For these reasons, they are not recorded here. + +- **"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"](/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". \ No newline at end of file diff --git a/content/members.md b/content/members.md new file mode 100644 index 0000000..d86a453 --- /dev/null +++ b/content/members.md @@ -0,0 +1,28 @@ +--- +title: "Members" +--- + +# Co-founders + +- [Davide Barbarossa](https://davidebarbarossa12.github.io/index.html)
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)
Sequent calculus, deep inference, type theory, Peirce's existential graphs, focalization, proof search -- Ecole Polytechnique +- [Boris Eng 🦖](https://www.engboris.fr) (administrator)
Computer science, transcendental syntax -- OCamlPro / SuperBOL +- Valentin Maestracci
Lambda-calculus, type theory, homotopy type theory, Dedukti, directed homotopy theory, rewriting -- Université Aix-Marseille + +# Members + +- 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)
+- Jérémy Hervé 🍄
Mushrooms -- Independent
+- [Ambroise Lafont](https://amblafont.github.io/)
Type Theory and Category Theory -- University of Cambridge
+- Luc Pommeret +- Adrien Ragot
Proof-nets, interaction nets, implicit computational complexity, lambda-calculus, linear logic -- Université Sorbonne Paris Nord / University Roma Tre
+- Paul Séjourné
Philosophy (Aristotle, Kant, Deleuze), algebraic geometry, category theory -- Université Paris-Sorbonne
+- Vincent 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 -- École normale supérieure de Lyon
+- [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. \ No newline at end of file diff --git a/content/projects.md b/content/projects.md new file mode 100644 index 0000000..9ce91ec --- /dev/null +++ b/content/projects.md @@ -0,0 +1,5 @@ +--- +title: "Projects" +--- + +(Soon...) \ No newline at end of file diff --git a/content/resources.md b/content/resources.md new file mode 100644 index 0000000..79dab79 --- /dev/null +++ b/content/resources.md @@ -0,0 +1,13 @@ +--- +title: "Resources" +--- + +- [*"An exegesis of transcendental syntax" (PhD thesis)* -- Boris Eng](https://hal.science/tel-04179276v1) +- [*"Information, Processes and Games" (section 1 & 5)* -- Samson Abramsky](https://arxiv.org/abs/1604.02603) +- [*"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) \ No newline at end of file diff --git a/go.mod b/go.mod new file mode 100644 index 0000000..7a9f208 --- /dev/null +++ b/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 diff --git a/go.sum b/go.sum new file mode 100644 index 0000000..405116a --- /dev/null +++ b/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= diff --git a/hugo.toml b/hugo.toml new file mode 100644 index 0000000..056cc83 --- /dev/null +++ b/hugo.toml @@ -0,0 +1,94 @@ +baseurl = "https://example.com" +copyright = "© ReFL, website based on Will Fraught's Paige theme for Hugo" +enablerobotstxt = true +languagecode = "en-us" +paginate = 50 +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 = "projects" +name = "Projects" +url = "/projects/" +weight = 30 + +[[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" + +[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" +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.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)" + +[params.paige.file_link] +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/home.html b/layouts/home.html new file mode 100644 index 0000000..1f455a4 --- /dev/null +++ b/layouts/home.html @@ -0,0 +1,7 @@ +{{ define "main" }} +{{ $page := . }} + +{{ partial "paige/article.html" $page }} +{{ partial "paige/pages.html" $page }} + +{{ end }} diff --git a/layouts/partials/paige/footer-first.html b/layouts/partials/paige/footer-first.html new file mode 100644 index 0000000..7c9331b --- /dev/null +++ b/layouts/partials/paige/footer-first.html @@ -0,0 +1 @@ +
\ No newline at end of file diff --git a/layouts/partials/paige/main-first.html b/layouts/partials/paige/main-first.html new file mode 100644 index 0000000..1d6667d --- /dev/null +++ b/layouts/partials/paige/main-first.html @@ -0,0 +1 @@ +
\ No newline at end of file diff --git a/layouts/partials/paige/style-first.css b/layouts/partials/paige/style-first.css new file mode 100644 index 0000000..025832b --- /dev/null +++ b/layouts/partials/paige/style-first.css @@ -0,0 +1,45 @@ +#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); +} + +.nav-link { + color: rgb(40, 173, 145); +} \ No newline at end of file diff --git a/static/images/zulip.png b/static/images/zulip.png new file mode 100644 index 0000000000000000000000000000000000000000..d38b5e804d57dfe31aafad04ed1c6147958aaeab GIT binary patch literal 3237 zcmV;W3|jMvP)>R`YsIO1318nX8j;&T> z)j1OC@K1G4b#CFVnEb06Uzu2olnJ$%#*@{^U!P$ZBWGBQP4(3vdHmz}vM{kXc|m-T zclY0XJmG9JgTppWtihDTTKx6z&)@@M^kb4-jra48`xo!L2sivRgG-(A)gi2IGD-q? zpBPz8cvpRoC;mZph{0nHv1wexPsGq-;;Y855^L~eLJf$)^Q!R{FNAUCPUIl>-nmh} z#A>YM&(PFzUkxUhh0r4tYw&lT_+_d|abjs=75*yBojd#>sR~bVGZ3d<^i|@gBHl9Y zNqji55|g+A?F@0QjW@wVycs?u;vrn{pLp`O_iBW()mM!_X#E5Zuk;6#Dj^yAWDswT zfVzg%YuA_K=Um)621|@J+_RtPGWqFA6*$LW3`rCBF4xQV@ZXbCi7Cky!0;K|!$lwvu9VV~qER!op5MLYfmvmDjw8phfFcyvJ+tJg)az=WXV7M30 z(Su?vk`czA_zw_+;cAo~!EeQAW?TRt<`ZvYFgzec>qqsbAR{OzWrPS$DJmyi{}|!E z=Lz?_+Di1R!A_S{5jG!&Hc^ZC;!0JUz4)e}W@M8e#^3F}&{xzDj+}*dIeZ4V ztlIuXkQu@shyA~LnG0zNgI#h$gsn%QZMGi;azmb;1Ytk?}zv)w2+fbWRGl09EO zl+6R|w&N(`CfknyPV_iup1e;C6!rXZ_B=YsV7Cni5I0$~7pi6_98_~W!0yL5hb|Zz zw;^uw+9t;q0N)hgZ=%2ORYWw04{|~zMu?Y$-cmI?BX_HHtHbao(KERLIW0FpaMBG`gqC(_o8~s) zs!~;})8wOlECAZV;IzOi1cH8%1k8R()#wWAyWjcq<173_xW)X}2pv+d$yW>8O+C&E z;7gqgU=C7q=MdcFwi?3bgYbM>+kt7%shV8Ik3{kRPW$IbvZRk*sIx8C_L-&{YP9r$45 z`f`Glu#|nrfvX~}uj!Nk-X#iW;k)^>3C6%;n_(#%_W>8r_eM>HGw}_PHw)tiKG3+K z%-Zf>wjC%5c&Dy{+4wu({^Rn24>V$%Flb&}0~Gi@R+}FeiGrDOQo$@j-;5he2j2a} zY8pLS-)#A?;4f+z`eqEY``aZDc)`o{$tu1Epw}6CGj5Fbzx&m50+Sy1e2uS&!kM&= zAs*ZmB{Xh=#pCq2_; zq-X~1Qw!h}gU%*BMrdvYBmp-^t&NFoM6YZ=2wX8wtKOUtyb78abhYrs&Q}(B_gfg# z_wHZ01GvbqU4PDtqUqGZprhItfzbJq>@5*%<6;}oEpM&|N@i-=qYhpGvV%b`h_$&h97n#Ny6z8sY^oO*S#;;=-8{OScgIm(JZEwl+StfuJHK5Pq4| z&vbTP6i<_<7<6#O9EmOa(JMTumd4*4QoA2ekMXBJ-Z@5NC)5JiuR}36E|fTUqVKn3 z-5R!bj>ZjybIrg5)tx`n++I;KRjw_bD&b{!MkP+1MW2bSC(Gw~dn4iIp!zyaOp&WZ z@l<-17XiF#QZ1pWrT;f${=2<%0CFV>18|>ho26r!XWLhHJ;Y9Cvg}o~K6`O^wr$(C zZBBRp*Zr*Z?#yJ;U)2}mSDcy2t!wzYQZ^cOu4KKsR8mMse;LH!qz0UZAN>tqU)r^j z_TU3R%hNIV9^)Hcl=!z9X^vmQ%qgVnz$`#mvU-HwsP`G zx&-X3rZ96kYu17oc{Q@ZO{;x??3M6zIt1(ap2Cv#44T8#CGyeV93ACi0}}vO*~;kw zE|^v27YZA9G=DLy{J)xUyVBEt3m4eR$rQ5&ifbtBIRMRO@meOE+YIgHWD+`yt&CQ2 z!EBaxqvD&n79qaIowI@&>iBsK`b=O@P$Tj%t!3yed>X#B^ApYFFa6Jb#!qWjZw83f zi=51*t(1I;&f-eK!}d}NX0dK41IoZMPzq2tjDeYI>_}a*?O}f63Nr*&GsK$f3S!)v z!6q4kGP)RDiY-N}j1DaOS1Mk^EsMx4{|}L?;g+IHaV50(9VrS%I(G#Ft228U1EcHg zOlohVOL2b(H}Es}8x@rLBL&L9@`xOBelc_a_I-=tdUPcm30mh!QZT|E8MM0iZX=k; z*%%Y_Pt*|h1o_y>FJy$%7BR>aW-ex6RGl3u?LE{G7{j%$B;9I6V9VDt$P`wrH*5eJ zUs<$(Unt>BP|(};TOnf*xf)SpN1PU;rf|gJSyzHGF6il!H4HL^MXQ*|S#Oy=4o{=z z;EJ;$t~dof9Y32vrZ9FU1HJ3(jI)8LxwzumTY3lhYi|ab!p}YR9{_i(g`19Z$LJg` z=w%>9;ouRlJO>Ve$QAUgtt&>Rqn6@Hkk9oDQaE5N1FO?_Gy}cs>WPt$P-}3<$P7IL z^(82*-3*px{T2{8>O25s=DC0Vv=ncN_P(ctf}Y|ZDD2(`mSfjmfV}TTj{52<(%wRC z!BfnJ=pA%UHHFn1z%r~{&mg->|K_`6v^#1m{y04ADW)g5pr>ALT|Wk^)~DzH14PWC z@il!JctuY7d(dADkD&H|-&m3hMj1{~i2Xw0hkqFS_^-JYF^X8jDG|G&22gw9uYjBQ z6tD6YQAi7=i_d-M-(L9mn+bly%=F1islO0jMIC{!h*p_Ad1)anK^=wo*O0G}&gX*E ze0mGWv~y4W9fiLTp67RVmcD8FzxQg6r_gQP4og8fq26az-+it$xGQ7@x~k(NhArk1u&f*zyzeaI?I9K zR%8Z(814;XZFwM{fK&%DS?$e&2auWYVR+JywUr&4yj0XUm<>-LGZKx$J;6LOjSKCs zG?YhXg)rQY%#3(l;=vAY=j5fiWQ-fb?I<0<7_JZIlWy&nylj3SjNwL%S9$O=R-JQ~U&lei#l+F%Zup<;Lv zSqZV^aVST_JVDxE@=_Mc)vCL6f$NY}2}iZp!`XCkIGcdJ& zKPVedjzn@aEIv7*Oe2Ef;ZQcI&*0_{QWSU`Wjc{8?d?bwnaG6ogpl#)$8MJ+>;oehtvDphy^H*g`%+#1Q! z65$+p21(lfsX4-}QuC<@uf_rav@)*9EJx~m3++`P{H>nbN6$hgWS)ZB