December 2021 - Categories - categories.org.au

Re: "First" use of 'Category theory' to describe our field
by David Roberts 23 Feb '24

23 Feb '24

Dear Ross, no, that's pretty good! It's mildly surprising that it took ~20 years for the name to 'stick', but maybe less so given that the field grew slowly to start. Thanks, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Thu, 11 Jul 2019 at 08:21, Ross Street <ross.street(a)mq.edu.au> wrote: > > Dear David > > From memory, the Pure Mathematics Honours (USyd) course that Max Kelly taught in 1965 > was called ``Category Theory''. It concentrated on different kinds of morphisms > and factorizations in a category, and finished with adjoint functors. > Also John Gray's (UIllinois) 1968-69 graduate course had that name. > > From Eilenberg I heard that each person using categories should have their own category of expertise. > I told this to John Gray who said that was fine; the time had come for that category to be Cat. > > I would suggest that the first category theorists to think of themselves as such were Eilenberg's students at Columbia. > However, Mac Lane was definitely a category theorist. > > This is probably not the verifiable stuff you were seeking. > > Ross > > > On 10 Jul 2019, at 10:01 PM, David Roberts <droberts.65537(a)gmail.com> wrote: > > Hi all, > > the (idle) question is: when did the phrase 'category theory' catch on > for the field? Clearly it didn't leap from either of the heads of > Eilenberg or Mac Lane full-grown, since they used the phrase 'General > theory of natural equivalences'. There are the old 'Reports of the > Midwest Category Seminar' lecture notes (the first in 1967), which > hints that 'category theory' wasn't quite the name in use. > > Even more interesting: who was the first "category theorist", by that name? > > Answers referring to verifiable sources would be best. > > Thoughts? > > David > > > > David Roberts > Webpage: https://ncatlab.org/nlab/show/David+Roberts > Blog: https://thehighergeometer.wordpress.com > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 4

Francois Lamarche's new email address
by Francois Lamarche 31 Dec '21

31 Dec '21

Greetings to all. Exactly one year ago I retired from my job at INRIA. I then lost my online presence there but got them to redirect all mails sent to my old professional addresses to francois.inria(a)sfr.fr I was aware that stuff would get lost once in a while, but it's hard to tell what proportion, given that e.g., I seem to get everything that is sent on this very list. Paul Taylor suggested that I send the present msg to tell people that they should update their email contact for me to the aforementioned. Happy holidays to everyone, Fran??ois Lamarche [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ETAPS Test of Time Award 2022, call for nominations
by Tarmo Uustalu 28 Dec '21

28 Dec '21

The ETAPS Test of Time Award recognizes outstanding papers published more than 10 years in the past in one of the constituent conferences of ETAPS. The Award recognises the impact of excellent research results that have been published at ETAPS. See https://etaps.org/about/test-of-time-award . Nominations Nominations for the 2022 ETAPS Test of Time Award are solicited from the ETAPS community. A nomination should include the title and publication details of the nominated paper, explain the influence it has had since publication, and why it merits the award. The nomination should phrase it in terms that are understandable by the members of the award committee and suitable for use in the award citation and should be endorsed by at least 2 people other than the person submitting the nomination. Self-nominations are not allowed. Nominations should be sent by Monday 14 February 2022 to the chair of the award committee, Don Sannella <dts(a)inf.ed.ac.uk>. Award committee The 2022 award committee consists of Rance Cleaveland, Ugo Dal Lago, Marieke Huisman, Jan Křetínský, Don Sannella (chair), Gabriele Taentzer and Peter Thiemann. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Topos Colloquium 2021 Retrospective and 2022 Prospective
by David Spivak 17 Dec '21

17 Dec '21

Dear category theorists, As many of you know, Topos Institute is a new non-profit research institute, dedicated to using category theory and related disciplines to shape technology for public benefit. You can find our 2021 retrospective in our blog https://topos.site/blog/. We've had a very successful colloquium in 2021 consisting of around 40 talks—both pure and applied—from speakers such as Awodey, Baez, Riehl, Avigad, and many more. A complete list—as well as slides and links to YouTube videos—can be found here https://topos.site/topos-colloquium/ The colloquium will start again in February 2022. If you'd like to sign up for announcements, please send an email to seminars+subscribe(a)topos.institute (with any content or subject line; it will all be ignored by the automated system.) If you need to contact us for something else, email us at info(a)topos.institute We'd love to have you join us next year! Best regards, and happy holidays, David, for the team at Topos [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CfParticipation LACompLing2021 / Logic and Algorithms in Computational Linguistics 2021, MALIN, Montpellier
by Roussanka Loukanova 13 Dec '21

13 Dec '21

Call for Participation Symposium Logic and Algorithms in Computational Linguistics 2021 (LACompLing2021) 15 - 17 December 2021, Online https://staff.math.su.se/rloukanova/LACompLing2021-web/ Online streaming by CNRS, Montpellier, France https://malin2021.sciencesconf.org LACompLing2021 is part of the week Mathematical Linguistics (MALIN) 2021, Université de Montpellier, LIRMM, CNRS, Montpellier, France 13--17 December 2021, Online ==== PROGRAM WEDNESDAY DECEMBER 15 / Wed 15 Dec 09:00-9::40 Wed 15 Dec Stefan Müller (Humboldt-Universität zu Berlin, Germany) The CoreGram Project: Deriving Crosslinguisitc Generalizations with HPSG Grammars of Multiple Languages (Invited Talk) 9:40-10:20 Wed 15 Dec Lars Hellan (Norwegian University of Science and Technology, Norway) A Unified Valence Resource (Invited Talk) 10:20-10:40 Break 10:40-11:00 Wed 15 Dec Luuk Suurmeijer (Heinrich Heine University Düsseldorf), Noortje Venhuizen (Saarland University) and Harm Brouwer (Saarland University, Germany) Compositionality in Distributional Formal Semantics 11:00-12:00 Wed 15 Dec Michael Moortgat (Utrecht University, Netherlands) Dependency Relations, Modalities and the Syntax-Semantics Interface (Keynote Talk) 12:00-13:30 Lunch break 13:30-14:10 Wed 15 Dec Stepan Kuznetsov (Steklov Mathematical Institute, RAS, Russia) Complexity of the Lambek Calculus and Its Extensions (Invited Talk) 14:10-14:30 Wed 15 Dec Renhao Pei (Utrecht University, Netherlands) Generating Pragmatically Appropriate Sentences from Propositional Logic: the Case of Conditional and Biconditional 14:30-15:30 Wed 15 Dec Christian Retoré (Université de Montpellier and LIRMM-CNRS, France) Inferentialism and Natural Language Semantics, with a Focus on Quantifiers (Keynote Talk) 15:30-15:50 Break 15:50-16:30 Wed 15 Dec Denis Bechet (LS2N - University of Nantes, France) and Annie Foret (IRISA, University of Rennes 1, France) Categorial Dependency Grammars: Analysis and Learning (Invited Talk) 16:30-17:30 Wed 15 Dec Tracy King (Adobe, United States) White Roses, Red Backgrounds: Bringing Structured Representations to Search (Keynote Talk) THURSDAY DECEMBER 16 / Thu 16 Dec 09:00-09:20 Thu 16 Dec Hitomi Yanaka (The University of Tokyo, Japan) Towards Compositional Semantics and Inference System for Telicity 09:20-09:40 Thu 16 Dec Daisuke Bekki, Ribeka Tanaka and Yuta Takahashi (Ochanomizu University, Japan) Integrating Deep Neural Network with Dependent Type Semantics 09:40-10:20 Thu 16 Dec Zhaohui Luo (Dept of Computer Science, Royal Holloway, Univ of London, United Kingdom) Universes in Type-Theoretical Semantics (Invited Talk) 10:20-10:40 Break 10:40-11:20 Thu 16 Dec Kristina Liefke (Ruhr University Bochum, Germany) Meaning-Driven Combinatorial Restrictions and 'imagine *whether' (Invited Talk) 11:20-12:00 Thu 16 Dec Alexey Stukachev (Sobolev Institute of Mathematics, Novosibirsk State University, Russia) Generalized Computability and Effective Model Theory in Mathematical Linguistics (Invited Talk) 12:00-13:30 Lunch break 13:30-14:30 Thu 16 Dec Richard Moot, (Université de Montpellier and LIRMM-CNRS, Montpellier, France Graph Rewriting as a Universal Proof Theory for Modern Type-Logical Grammars (Keynote Talk) 14:30-15:30 Thu 16 Dec Randy Harris (University of Waterloo, Canada) Rhetorical Figures as Algorithms (Keynote Address) FRIDAY DECEMBER 17 / Fri 17 Dec 09:00-10:00 Fri 17 Dec Aarne Ranta (University of Gothenburg, Sweden) Abstract Wikipedia and Vastly Multilingual Natural Language Generation (Keynote Talk) 10:00-10:20 Fri 17 Dec Inari Listenmaa (Singapore Management University, Singapore), Martin Strecker (Singapore Management University, Singapore) and Warrick Macmillan (University of Gothenburg, Sweden) Natural Language Generation and Processing for the Legal Domain 10:20-10:40 Break 10:40-11:20 Fri 17 Dec Bjoern Jespersen (Utrecht University, Netherlands) Impossibilities without Impossibilia (Invited Talk) 11:20-12:00 Fri 17 Dec Marie Duzi (VSB-Technical University of Ostrava, Czechia) Questions and Answers on Dynamic Activities of Agents (Invited Talk) 12:00-13:30 Lunch break 13:30-13:50 Fri 17 Dec Symon Jory Stevensguille (The Ohio State University, United States) Decomposing Events into GOLOG 13:50-15:30 Fri 17 Dec Lasha Abzianidze (Utrecht University, Netherlands) How to Train a Theorem Prover for Natural Language Inference (Invited Talk) 15:30-16:00 Break 16:00-17:00 Fri 17 Dec Larry Moss (Indiana University Mathematics Department, United States) Monotonicity in Natural Language Inference: Theory and Practice (Keynote Talk LACL / LACompLing2021) ==== [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ICGT 2022: Call for Papers
by Daniel Strüber 10 Dec '21

10 Dec '21

======================================================= 15th International Conference on Graph Transformation ICGT 2022 - https://icgt2022.gitlab.io/ July 7-8, Nantes, France, co-located with STAF 2022 ======================================================= AIMS AND SCOPE The use of graphs and graph-like structures as a formalism for specification and modelling is widespread in all areas of computer science as well as in many fields of computational research and engineering. Relevant examples include software architectures, pointer structures, state space and control/data flow graphs, UML and other domain-specific models, network layouts, topologies of cyber-physical environments, quantum computing and molecular structures. Often, these graphs undergo dynamic change, ranging from reconfiguration and evolution to various kinds of behaviour, all of which may be captured by rule-based graph manipulation. Thus, graphs and graph transformation form a fundamental universal modelling paradigm that serves as a means for formal reasoning and analysis, ranging from the verification of certain properties of interest to the discovery of fundamentally new insights. The International Conference on Graph Transformation aims at fostering exchange and collaboration of researchers from different backgrounds working with graphs and graph transformation, either in contributing to their theoretical foundations or by applying established formalisms to classical or novel areas. The conference not only serves as a well-established scientific publication outlet, but also as a platform to boost inter- and intra-disciplinary research and to leeway for new ideas. The 15th International Conference on Graph Transformation (ICGT 2022) will be held in Nantes, France, as part of STAF 2022 (Software Technologies: Applications and Foundations). The conference takes place under the auspices of EATCS and IFIP WG 1.3. Proceedings will be published by Springer in the Lecture Notes in Computer Science (LNCS) series. IMPORTANT DATES - Abstract submission: February 21, 2022 - Paper submission: February 28, 2022 - Notification: April 18, 2022 - Camera-ready: May 9, 2022 - Conference: July 7-8, 2022 Note: All times are end-of-day Anywhere on Earth. SUBMISSIONS - TOPICS OF INTEREST In order to foster a lively exchange of perspectives on the subject of the conference, the programme committee of ICGT 2022 encourages all kinds of contributions related to graphs and graph transformation, either from a theoretical point of view or a practical one. Topics of interest include, but are not limited to the following subjects: - General models of graph transformation (e.g. adhesive categories and hyperedge replacement systems) - Analysis and verification of graph transformation systems - Graph theoretical properties of graph languages - Automata on graphs and parsing of graph languages - Logical aspects of graph transformation - Computational models based on graphs - Structuring and modularization of graph transformation - Hierarchical graphs and decomposition of graphs - Parallel, concurrent, and distributed graph transformation - Term graph and string diagram rewriting - Petri nets and other models of concurrency - Business process models and notations - Bigraphs and bigraphical reactive systems - Graph databases and graph queries - Model-driven development and model transformation - Model checking, program analysis and verification, simulation and animation - Syntax, semantics and implementation of programming languages, including domain-specific and visual languages - Graph transformation languages and tool support - Efficient algorithms (e.g. pattern matching, graph traversal, network analysis) - Applications and case studies in software engineering (e.g. software architectures, refactoring, access control, and service-orientation) - Applications to computing paradigms (e.g. bio-inspired, quantum, ubiquitous, and visual) - Graph transformation and artificial intelligence (e.g., AI for graph transformations, applying graph transformations in AI engineering and search-based software engineering) - SPECIAL INTEREST TOPIC OF ICGT 2022: EXECUTABLE APPLIED CATEGORY THEORY A special focus of this conference will consist of new approaches to formalizing the knowledge in the research field of graph transformation theory via proof assistants such as Coq. Referring to the homepage of the GReTA-ExACT workgroup for further information [1], a long-term goal of this kind of approach will consist in establishing a Coq-enriched wiki for our research field akin to the nLab. This platform will serve as a sustainable mechanism for curating applied and mathematical knowledge in graph transformation research, and eventually as a research tool in its own right, notably through the provision of interactive database-supported proof construction. Another avenue of research will concern executable applied category theory (ExACT), i.e., code extraction from formalized categorical structures, with the perspective of curating a database of correct-by-construction reference prototype algorithms for various forms of graph transformation semantics and graph-like data structures. To introduce the initiative and facilitate the broad involvement of the ICGT community and collect feedback from participants regarding the scope and format of such a wiki project, a peer-reviewed brainstorming session is planned as one of the events at the conference. - SUBMISSION GUIDELINES Papers can be submitted via EasyChair [2] using Springer???s LNCS format (cf. LNCS Overleaf template [3]). For regular and tool demonstration papers, simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. The page limits are strict and include references. At least one author for each accepted paper must register before the early registration deadline and present the paper during the conference [4]. Papers are solicited in three categories: - Regular papers (limited to 16 pages in Springer LNCS format) describe innovative contributions and are evaluated with respect to their originality, significance, and technical soundness. We also solicit case studies describing applications of graph transformation in any application domain. Additional material intended for reviewers but not for publication in the final version may be included in a clearly marked appendix. - Tool presentation papers (limited to 8 pages in Springer LNCS format) demonstrate the main features and functionality of graph-based tools. A tool presentation paper may have an appendix with a detailed demo description (up to 4 pages), which will be reviewed but not included in the proceedings. - New ideas papers (limited to 2 pages in Springer LNCS format) report on relevant contributions to the theory or applications of graph transformation, which may have been published (or accepted for publication) in a peer-reviewed conference other than ICGT, as a book chapter or journal article since 2018. Papers in this category will be selected for presentation at the conference according to their relevance to the graph transformation community, and they will be considered for the special issues. Submissions will consist of a 2-page abstract. In case of extended abstracts of published papers, the submission must refer to the published paper and include the original paper in PDF. SPECIAL ISSUE Authors of the best papers at the conference will be invited to prepare and submit extended journal versions to be considered for publication in a special issue after an independent round of peer review (details TBA). PROGRAM & LOCAL INFORMATION TBA on the conference website [5]. ORGANIZATION Program Chairs - Nicolas Behr (CNRS, IRIF, Universit?? de Paris, France) - Daniel Str??ber (Chalmers | University of Gothenburg, Sweden, and Radboud University, Netherlands) Program Committee - Paolo Baldan (Universit?? degli Studi di Padova, Italy) - Paolo Bottoni (Sapienza Universit?? di Roma, Italy) - Andrea Corradini (University of Pisa, Italy) - Juan de Lara (Universidad Aut??noma de Madrid, Spain) - Juergen Dingel (Queen???s University Kingston, Ontario, Canada) - Fabio Gadducci (University of Pisa, Italy) - Holger Giese (Hasso Plattner Institute, University of Potsdam, Germany) - Russ Harmer (CNRS, ENS Lyon, Universit?? de Lyon, France) - Reiko Heckel (University of Leicester, United Kingdom) - Thomas Hildebrandt (University of Copenhagen, Denmark) - Wolfram Kahl (McMaster University, Canada) - Timo Kehrer (Humboldt-Universit??t zu Berlin, Germany) - Aleks Kissinger (University of Oxford, United Kingdom) - Barbara K??nig (Universit??t Duisburg-Essen, Germany) - Leen Lambers (Technical University of Brandenburg (BTU) Cottbus-Sentenberg, Germany) - Yngve Lamo (Western Norway University of Applied Sciences Bergen, Norway) - Koko Muroya (RIMS, Kyoto University) - Fernando Orejas (Universitat Polit??cnica de Catalunya) - Detlef Plump (University of York, United Kingdom) - Arend Rensink (University of Twente Enschede, Netherlands) - Leila Ribeiro (Federal University of Rio Grande do Sul (UFRGS) Porto Alegre, Brazil) - Andy Sch??rr (Technische Universit??t Darmstadt, Germany) - Gabriele Taentzer (Philipps-Universit??t Marburg, Germany) - Matthias Tichy (Universit??t Ulm, Germany) - Uwe Wolter (University of Bergen, Norway) - Steffen Zschaler (King???s College London, United Kingdom) CONTACT All questions about submissions should be emailed to icgt2022.info(a)gmail.com. LINKS [1] GReTA ExACT: International Online Workgroup on Executable Applied Category Theory for Rewriting Systems https://www.irif.fr/~greta/gretaexact/ [2] EasyChair submission site: https://easychair.org/conferences/?conf=icgt2022 [3] LNCS Template: https://www.overleaf.com/latex/templates/springer-lecture-notes-in-computer… [4] STAF 2022 Registration: https://staf2022.univ-nantes.io/registration/ [5] ICGT 2022: https://icgt2022.gitlab.io/ -- Dr. Daniel Str??ber https://www.danielstrueber.de/ Senior Lecturer Department of Computer Science and Engineering Chalmers University of Technology | University of Gothenburg Assistant Professor Department of Software Science Radboud University Nijmegen [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: CANCELLED: GReTA-ExACT online workgroup, Friday December 10
by Reiko Heckel 08 Dec '21

08 Dec '21

FYI, I hope this comes in time … On 07/12/2021, 18:30, "GReTA Seminar organisers" <greta(a)irif.fr> wrote: Dear colleagues, Unfortunately, due to unforeseen complications in the overseas travels of our speaker, we must CANCEL the workgroup event which was originally planned for Friday, December 10. The workgroup sessions will continue in February 2022 (details TBA). With best regards, Nicolas Behr, Andrea Corradini, Jean Krivine and Reiko Heckel (GReTA organisers) ---------------------------------------------------------------------------- GReTA - Graph TRansformation Theory and Applications International Online Seminar Series ---------------------------------------------------------------------------- Contact: greta(a)irif.fr<mailto:greta@irif.fr> Webpage: www.irif.fr/~greta YouTube: https://www.youtube.com/channel/UC6j-G6oPmkqCgOx6UQOUhSQ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Invitation: GReTA-ExACT online workgroup, Friday December 10, 2021, 15:00 CET
by Reiko Heckel 06 Dec '21

06 Dec '21

FYI, Reiko On 06/12/2021, 08:37, "GReTA Seminar organisers" <greta(a)irif.fr> wrote: Dear colleagues, It is our great pleasure to invite you to the next session of the “GReTA-ExACT - Executable Applied Category Theory” online workgroup: Friday December 10, 15:00 CET "Formalizing Category Theory using Type Theory: A Discussion", E.J. Gallego Arias (abstract, Zoom and YouTube links attached below) In the context of the GReTA - "Graph TRansformation Theory and Applications" online seminar series hosted at IRIF (https://www.irif.fr/~greta/) the GReTA ExACT (Executable Applied Category Theory) online workgroup aims at providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and repository for mathematical knowledge in our research field (akin to a domain-specific Coq-enabled variant of the nLab). A further research question will consist in exploring the possibility for deriving reference prototype implementations of concrete rewriting systems (e.g., over multi- or simple directed graphs) directly from the category-theoretical semantics, in the spirit of the translation-based approaches (utilizing theorem provers such as Microsoft Z3). Please refer to https://www.irif.fr/~greta/gretaexact/ for further details (including information on how to register for participating in the Zoom meetings). With best regards, Nicolas Behr, Andrea Corradini, Jean Krivine and Reiko Heckel (GReTA organisers) ___________________________________________________ Date and time: Friday December 10, 2021, 15:00 CET Title: Formalizing Category Theory using Type Theory: A Discussion Speaker: Emilio Jesús Gallego Arias (Université de Paris, CNRS, IRIF, France) Abstract: Since its inception at the start of the 20th century, type theory has become a core foundational tool for those interested in the logical foundations of mathematics and computer science. A key milestone on the field is the Calculus of Inductive Constructions, the type theory that lies at the heart of modern interactive proof assistants such as Coq or Lean. The CiC is remarkably expressive, yet remains computationally tractable, leading to important milestones in computer-checked mathematical results such as the 4 color theorem or the Feit-Thompson theorem. In this talk, we will present the calculus of inductive constructions as currently implemented in the Coq proof assistant, and we will explore the encoding of basic constructions of category theory in Coq, placing a particular emphasis the usability and modularity of our definitions. Zoom registration link: https://u-paris.zoom.us/meeting/register/tZwrdO2hrDssHtEB5TYi6tZPmm2hn1QCrs… Link to YouTube live stream: https://youtu.be/lM0b3oHDunU ___________________________________________________ ---------------------------------------------------------------------------- GReTA - Graph TRansformation Theory and Applications International Online Seminar Series ---------------------------------------------------------------------------- Contact: greta(a)irif.fr Webpage: www.irif.fr/~greta<http://www.irif.fr/~greta> YouTube: https://www.youtube.com/channel/UC6j-G6oPmkqCgOx6UQOUhSQ Twitter: https://twitter.com/GReTAseminars [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

PhD position on Quantitative Semantics at INESC-TEC and University of Minho.
by Renato Neves 04 Dec '21

04 Dec '21

We [2] have available a PhD studentship on the topic of quantitative semantics for hybrid programming [1]. The position will involve (extensions of) lambda-calculus and category theory. We will also work with bits and pieces of topology and probability theory. But don't worry if you're unfamiliar with some of these topics -- most important is that you're eager to learn! * Starting date The starting date is preferably 1st April 2022. * Context This position is part of a broader research project that involves several researchers across different institutions in the north of Portugal. The overarching goal is to establish mathematical foundations for a discipline of hybrid programming capable of handling noise and uncertainty in a principled, rigorous way. In case you're not familiar with the concept, a hybrid program combines classical program constructs with differential equations to model, among other things, interactions between digital devices and physical processes (such as velocity, movement, and energy). Examples of hybrid programs can be found in [1,6] and in my webpage. * How to apply Please send me an email no later than 22nd December 2021 with the following two items: + a cover letter; + a detailed CV. In the meanwhile if you have any questions about the position, including living in Portugal, please do not hesitate to contact me! Btw, Portugal is known as one of the safest countries in the world [3]; has lots of sunshine, pristine beaches, and great food [4,5]. -- Renato Neves https://di.uminho.pt/~nevrenato/ References: [1] Sergey Goncharov, Renato Neves, and José Proença. "Implementing hybrid semantics: From functional to imperative." International Colloquium on Theoretical Aspects of Computing. Springer, Cham, 2020. (https://arxiv.org/abs/2009.14322) [2] https://www.inesctec.pt/en [3] https://en.wikipedia.org/wiki/Global_Peace_Index#Global_Peace_Index_2021_ra… [4] https://www.youtube.com/watch?v=akcDhdxSsCM [5] https://edition.cnn.com/travel/article/portugal-food/index.html [6] http://arcatools.org/assets/lince.html#fulllince [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Post-doc position in RECIPROG project (located in Lyon, Nantes or Paris)
by Alexis Saurin IRIF 03 Dec '21

03 Dec '21

This is an announcement for a postdoctoral position funded by the ANR ReCiProg - Reasoning on Circular proofs for Programming. *We seek candidates holding a PhD in Computer Science or Mathematics, and with expertise in one or several of the following areas:* - Proof theory - Curry-Howard correspondence - Logics with fixed points - Coinductive reasoning - Proof assistants - Type theory - Category theory - Automated deduction In relation with the above topics, an experience in one or several of the following topics will be particularly appreciated: fixed-points and circular proofs, the Coq proof assistant, inductive and coinductive types, guarded recursion, coalgebras, inductive and coinductive theorem proving. *The successful candidate will be employed in one of the following French research lab, depending on her/his specific profile:*- LIP (Plume Team), Lyon (local coordinator: Denis Kuperberg) - LS2N (Gallinette Team), Nantes (local coordinator: Guilhem Jaber) - IRIF (PPS & Picube Team), Paris (local coordinator: Alexis Saurin) *Application process:* - Deadline for applications is on January 5th 2022, for a starting date in the first trimester of 2022, to be negotiated. - Candidates can send their application to Alexis Saurin (alexis dot saurin at irif dot fr) with a subject containing “[RECIPROG post-doc application]”. - The application should contain a CV, a brief research statement (1-2 pages) & at least two contacts of reference persons (or reference letters if available). - The salary will depend on the successful candidate's prior research experience with a guaranteed minimum of 2300 EUR/month before taxes. *Project summary* RECIPROG is an ANR collaborative project (aka. PRC) starting in the fall 2021-2022 and running till the end of 2025. ReCiProg aims at extending the proofs-as-programs correspondence (aka Curry-Howard correspondence) to recursive programs and circular proofs for logics and type systems using induction and coinduction. The project will contribute both to the necessary theoretical foundations of circular proofs and to the software development allowing to enhance the use of coinductive types and coinductive reasoning in the Coq proof assistant. *More informations* - More informations can be found on the project webpage: https://www.irif.fr/reciprog/index and https://www.irif.fr/reciprog/post-doc-offer-dec2021 - RECIPROG ANR project will open further positions in the coming two years, including two more postdoctoral positions in the above teams, and a PhD position in LIRICA Team, LIS, Marseille. - Interested candidates may contact the project coordinator (Alexis Saurin) as well as the local coordinators (Guilhem Jaber, Denis Kuperberg, Luigi Santocanale & Alexis Saurin). -- Alexis Saurin IRIF - CNRS, Université de Paris & INRIA [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0