April 2022 - Categories - categories.org.au

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

24 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

DEADLINE EXTENSION: MFPS 2022: Conference on Mathematical Foundations of Programming Semantics
by Justin Hsu 30 Apr '22

30 Apr '22

========================================================= CALL FOR PAPERS: MFPS XXXVIII (MFPS 2022) 38th Conference on Mathematical Foundations of Programming Semantics July 11-13, 2022 Hybrid, from Ithaca, NY, USA https://www.cs.cornell.edu/mfps-2022/ ========================================================== IMPORTANT DATES (anywhere on earth): Abstract submission: May 3, 2022 Paper submission (EXTENDED): May 6, 2022 Author notification: June 10, 2022 Final version due: June 24, 2022 ========================================================== We are delighted to announce the 38th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2022). While the pandemic situation is uncertain, we plan to hold a hybrid conference with the in-person event at Cornell University in Ithaca, New York. MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged. Topics include, but are not limited to, the following: bio-computation; concurrent qualitative and quantitative distributed systems; process calculi; probabilistic systems; constructive mathematics; domain theory and categorical models; formal languages; formal methods; game semantics; lambda calculus; programming-language theory; quantum computation; security; topological models; logic; type systems; type theory. We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example. ------------------------------------------------- INVITED SPEAKERS: Barbara König, University of Duisburg--Essen Anca Muscholl, Université Bordeaux Daniela Petrisan, Université Paris Cité Frank Pfenning, Carnegie Mellon University ------------------------------------------------- SPECIAL SESSIONS: 1. Species of Structures in Algebra, Computation, and Logic Organizer: Marcelo Fiore, University of Cambridge Organizer: Nicola Gambino, University of Leeds 2. Relational Verification and Formal Reasoning Organizer: Marco Gaboardi, Boston University 3. Algebraic Effects Organizer: Ningning Xie, University of Cambridge ------------------------------------------------- PROGRAM COMMITTEE: Sandra Alves, University of Porto Arthur Azevedo de Amorim, Boston University Lars Birkedal, Aarhus University Steve Brookes, Carnegie Mellon University Jacques Carette, McMaster University Pierre Clairambault, CNRS and Aix-Marseille Université Jérémy Dubut, AIST, Tokyo Daniel Gratzer, Aarhus University Amar Hadzihasanovic, Tallinn University of Technology Masahito Hasegawa, Kyoto University Favonia, University of Minnesota Justin Hsu, Cornell University (co-chair) Achim Jung, University of Birmingham Delia Kesner, Université Paris-Diderot Isabella Mastroeni, Università di Verona Michael Mislove, Tulane University Renato Neves, Minho University Max New, University of Michigan Krishna S, IIT Bombay Taro Sekiyama, National Institute of Informatics, Tokyo Alexandra Silva, Cornell University Sam Staton, University of Oxford Christine Tasson, Sorbonne Université (co-chair) Maaike Zwart, IT University of Copenhagen ------------------------------------------------- MFPS ORGANIZERS: Andrej Bauer, University of Ljubljana Lars Birkedal, Aarhus University Stephen Brookes, Carnegie Mellon University Justin Hsu, Cornell University Achim Jung, University of Birmingham Catherine Meadows, Naval Research Laboratory Michael Mislove, Tulane University Joël Ouaknine, Max Planck Institute for Software Systems Prakash Panangaden, McGill University Alexandra Silva, Cornell University Sam Staton, University of Oxford Christine Tasson, Sorbonne Université ------------------------------------------------- LOCAL ORGANIZERS: Dexter Kozen, Cornell University Alexandra Silva, Cornell University ------------------------------------------------- SUBMISSION INSTRUCTIONS: Submissions should be made through EasyChair (<https://easychair.org/conferences/?conf=mfps2022>). Papers can be at most **15 pages** long, excluding bibliography, and should be prepared using the MFPS macros (<https://mfpsconf.org/?page_id=309>). ------------------------------------------------- PROCEEDINGS: A preliminary version will be distributed at the meeting. Final proceedings will be published in an open access journal after the meeting. ------------------------------------------------- CONTACT: For any further information about MFPS 2022, please contact the co-chairs: Justin Hsu (email(a)justinh.su) and Christine Tasson (christine.tasson(a)lip6.fr) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Applied Category Theory 2022: Second Call for Papers
by Jade Edenstar Master 27 Apr '22

27 Apr '22

5th Annual International Conference on Applied Category Theory (ACT2022) July 18–22, 2022 https://msp.cis.strath.ac.uk/act2022/ The Fifth International Conference on Applied Category Theory will take place at the University of Strathclyde from 18 to 22 July 2022, preceded by the Adjoint School 2022 from 11 to 15 July. This conference follows previous events at Cambridge (UK), Cambridge (MA), Oxford and Leiden. Applied category theory is important to a growing community of researchers who study computer science, logic, engineering, physics, biology, chemistry, social science, linguistics and other subjects using category-theoretic tools. The background and experience of our members is as varied as the systems being studied. The goal of the Applied Category Theory conference series is to bring researchers together, strengthen the applied category theory community, disseminate the latest results, and facilitate further development of the field. SUBMISSIONS We accept submissions in English of original research papers, talks about work accepted/submitted/published elsewhere, and demonstrations of relevant software. Accepted original research papers will be published in a proceedings volume. The keynote addresses will be chosen from the accepted papers. The conference will include an industry showcase event and community meeting. We particularly encourage people from underrepresented groups to submit their work and the organisers are committed to non-discrimination, equity, and inclusion. Submission formats: 1. Extended Abstracts should be submitted describing the contribution and providing a basis for determining the topics and quality of the anticipated presentation (1-2 pages). These submissions will be adjudicated for inclusion as a talk at the conference. Such work should include references to any longer papers, preprints, or manuscripts providing additional details. 2. Conference Papers should present original, high-quality work in the style of a computer science conference paper (up to 14 pages, not counting the bibliography; detailed proofs may be included in an appendix for the convenience of the reviewers). Such submissions should not be an abridged version of an existing journal article (see item 1) although pre-submission Arxiv preprints are permitted. These submissions will be adjudicated for both a talk and publication in the conference proceedings. 3. Software Demonstrations should be submitted in the format of an Extended Abstract (1-2 pages) giving the program committee enough information to assess the content of the demonstration. We are particularly interested in software that makes category theory research easier, or uses category theoretic ideas to improve software in other domains. Extended abstracts and conference papers should be prepared with LaTeX. For conference papers please use the EPTCS style files available at < http://style.eptcs.org>. The submission link is https://easychair.org/conferences/?conf=act2022. IMPORTANT DATES The following dates are all in 2022, and Anywhere On Earth. - Submission Deadline: Monday 9 May - Author Notification: Tuesday 7 June - Camera-ready version due: Tuesday 28 June - Adjoint School: Monday 11 to Friday 15 July - Main Conference: Monday 18 to Friday 22 July CONFERENCE FORMAT Assuming additional Covid restrictions will not be introduced in the UK, the conference will run as a hybrid event, with talks recorded or streamed for remote participation. Please be mindful of changing conditions when booking travel or hotel accommodations. FINANCIAL SUPPORT Limited financial support will be available for travel and accommodation. Priority will be given to people with financial need and those giving presentations. Please contact the organisers for more information. PROGRAM COMMITTEE Tai-Danae Bradley, City University of New York Benjamin Merlin Bumpus, University of Glasgow Matteo Capucci, University of Strathclyde Andrea Censi, ETH Zurich Corina Cirstea, University of Southampton Elena Di Lavore, Tallinn University of Technology James Fairbanks, University of Florida Zardini Gioele, ETH Zurich Jules Hedges, University of Strathclyde Kohei Kishida, University of Illinois, Urbana-Champaign Barbara König, University of Duisburg-Essen Clemens Kupke, University of Strathclyde Alexander Kurz, Chapman University Martha Lewis, University of Bristol (PC co-chair) Sophie Libkind, Stanford University Jade Master, University of Strathclyde (PC co-chair) Conor Mcbride, University of Strathclyde Joe Moeller, National Institute of Standards and Technology Elizabeth Munch, Michigan State University Fredrik Nordvall Forsberg, University of Strathclyde Paige North, University of Pennsylvania Emily Roff, University of Edinburgh Mehrnoosh Sadrzadeh, University College London Jonathan Sterling, Aarhus University Todd Trimble, Western Connecticut State University Christina Vasilakopoulou, University of Patras Greece Maaike Zwart, IT University of Copenhagen ORGANISING COMMITTEE Jules Hedges, University of Strathclyde Jade Master, University of Strathclyde Fredrik Nordvall Forsberg, University of Strathclyde James Fairbanks, University of Florida STEERING COMMITTEE John Baez, University of California, Riverside Bob Coecke, Cambridge Quantum Dorette Pronk, Dalhousie University David Spivak, Topos Institute [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Call for Presentations: VardiFest22
by Kristin Yvonne Rozier 24 Apr '22

24 Apr '22

============================================================ ??VardiFest22: On the Not So Unusual Effectiveness of Logic ???????????????????? (a collection of ~12-minute talks) ?????????? Technion, Haifa, Israel (co-located with FLoC) ???????????????????????????????????? July 31-August 1, 2022 https://vardifest.github.io/ ============================================================ VardiFest is a FLoC-22 workshop in honor of Moshe Y. Vardi and is intended to celebrate Vardi's pioneering contributions that have enhanced logic's centrality in computer science. The workshop will be organized in a Highlights conference style: i.e., composed of short talks and invited talks. This is a call for short talks (expected to be ~12 minutes). The proposal should be at most one page PDF in Easychair class style (https://easychair.org/publications/for_authors) Given the depth and breadth of Vardi's contributions that span across multiple fields of computer science and society at large, there is no definite list of topics of interest. We encourage you to present a proposal for a talk that would be of interest to Vardi be it published or not, technical or non-technical, retrospective or crystal-ball gazing. While we may allow some remote presentations, strong preference will be given to in-person presentations. ==================== DATES: ==================== Deadline for Submission: May 15, 2022 AoE Notification of Acceptance: May 19, 2022 AoE Submission Site: https://easychair.org/conferences/?conf=vardifest22 ==================== ORGANIZERS: ==================== Giuseppe De Giacomo (Sapienza Univ. Rome, Italy) Kuldeep S. Meel (National University of Singapore) Kristin Yvonne Rozier (Iowa State University, Ames, Iowa) View this Call in EasyChair: https://easychair.org/cfp/vardifest22 -- ____________________________________________________________ __ /\ \ \_____ / \ ###[==_____> / \ /_/ __ / __ \ \ \_____ | ( ) | ###[==_____> /| /\/\ |\ /_/ / | | | | \ / |=|==|=| \ Kristin Yvonne Rozier, Ph.D. / | | | | \ Black&Veatch Associate Prof, Iowa State Univ / USA | ~||~ |NASA \ Departments of Aerospace Engineering, |______| ~~ |______| Computer Science, Mathematics, and (__||__) Electrical and Computer Engineering /_\ /_\ Virtual Reality Applications Center !!! !!! laboratory.temporallogic.org [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, April 28, May 5 & 12
by Steve Awodey 24 Apr '22

24 Apr '22

~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ Mike Shulman (University of San Diego). April 28, May 5, May 12 11:30am-1:00pm EST (UTC-04:00) Join Zoom Meeting https://cmu.zoom.us/j/622894049 Meeting ID: 622 894 049 Passcode: the Brunerie number ************************************************************ Mike Shulman University of San Diego Towards Third-Generation HOTT In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure; but many desired equalities are not definitional, and univalence must be asserted by a non-computational axiom. Cubical type theories also define identity uniformly, but using paths instead. This makes more equalities definitional, and enables a form of univalence that computes; but requires inserting all the higher structure by hand with Kan operations. I will present work in progress towards a third kind of homotopy type theory, which we call Higher Observational Type Theory (HOTT). In this system, identity is not defined uniformly across all types, but recursively for each type former: identifications of pairs are pairs of identifications, identifications of functions are pointwise identifications, and so on. Univalence is then just the instance of this principle for the universe. The resulting theory has many useful definitional equalities like cubical type theories, but also gives rise to higher structure automatically like Book HoTT. Also like Book HoTT, it can be interpreted in a class of model categories that suffice to present all Grothendieck-Lurie (∞,1)-toposes; and we have high hopes that, like cubical type theories, some version of it will satisfy canonicity and normalization. This is joint work with Thorsten Altenkirch and Ambrus Kaposi. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

TCS assistant professorship at VU Amsterdam
by Fokkink, W.J. (WJ) 22 Apr '22

22 Apr '22

The Department of Computer Science at the Vrije Universiteit Amsterdam offers an open position as assistant professor in Theoretical Computer Science, broadly construed. https://workingat.vu.nl/ad/tenure-track-position-in-theoretical-computer-sc… Deadline for application is June 12, 2022. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Special Issue on Logic and Higher Structures in MSCS
by Samuel Mimram 22 Apr '22

22 Apr '22

Special Issue on Logic and Higher Structures in MSCS ==================================================== Dear everybody, There will be a special issue about logic and higher structures in the Mathematical Structures an Computer Science journal. Your contributions are welcome! Topic ----- Voevodsky's univalent foundations program has revealed deep connections between logic and homotopy theory, in particular via higher category theory. The goal of this special issue is to investigate these interactions, bringing together mathematicians from the communities of type theory, higher rewriting, higher category theory and homotopy theory. It follows the _Logic and Higher Structures_ conference which was held at CIRM, France, from 21 to 25 February 2022, although contributions not presented during the conference are also welcome. Submitting ---------- Submissions should be sent to lhs-mscs(a)lix.polytechnique.fr Important dates are - deadline for submissions: 1 July 2022 - notification of acceptance: 30 November 2022 Editors ------- The editors are - Dimitri Ara (Aix-Marseille Universit??) - Thierry Coquand (University of Gothenburg) - Philippe Malbos (Universit?? Claude Bernard Lyon 1) - Samuel Mimram (??cole Polytechnique) - Sinan Yalin (Universit?? d'Angers) You are welcome to contact them individually although the use of the global mail lhs-mscs(a)lix.polytechnique.fr is advised. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

28th WoLLIC 2022 - 3rd Call for Papers
by Ruy Jose Guerra Barretto de Queiroz 20 Apr '22

20 Apr '22

[Please distribute. Apologies for multiple postings] CALL FOR PAPERS WoLLIC 2022 28th Workshop on Logic, Language, Information and Computation September 20 to 23, 2022 Iași, Romania ORGANISATION Faculty of Computer Science, Alexandru Ioan Cuza University, Romania Centro de Informática, Universidade Federal de Pernambuco, Brazil CALL FOR PAPERS WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The twenty-eighth WoLLIC will be held at the Faculty of Computer Science, Alexandru Ioan Cuza University, Iași, Romania, September 20 to 23, 2022. It is scientifically sponsored by the European Association for Computer Science Logic (EACSL), the Interest Group in Pure and Applied Logics (IGPL), the The Association for Logic, Language and Information (FoLLI), the Association for Symbolic Logic (ASL) (tbc), the European Association for Theoretical Computer Science (EATCS) (tbc), and the Sociedade Brasileira de Lógica (SBL). ABOUT THE LOCATION Iași https://www.uaic.ro/en/iasi-2/ PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing, programming and Artificial Intelligence (AI); novel computation models and paradigms; broad notions of proof and belief; proof mining, type theory, effective learnability and explainable AI; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection; foundations of mathematics; philosophical logic; philosophy of language. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. Articles should be written in the LaTeX format of LNCS by Springer (see author's instructions at http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0) They must not exceed 12 pages, with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. (At least one author is required to pay the registration fee before granting that the paper will be published in the proceedings.) Papers must be submitted electronically at the WoLLIC 2022 EasyChair website https://easychair.org/conferences/?conf=wollic2022. PROCEEDINGS The proceedings of WoLLIC 2022, including both invited and contributed papers, will be published in advance of the meeting as a volume in Springer's LNCS series. In addition, abstracts will be published in the Conference Report section of the Logic Journal of the IGPL, and selected contributions will be published (after a new round of reviewing) as a special post-conference WoLLIC 2022 issue of Mathematical Structures in Computer Science (MSCS). INVITED SPEAKERS Anupam Das, University of Birmingham John Horty, University of Maryland Marie Kerjean, Université Sorbonne Paris Nord/CNRS Dorel Lucanu, Alexandru Ioan Cuza University Francesca Poggiolesi, Université Sorbonne/CNRS/IHPST IMPORTANT DATES April 30, 2022: Abstract deadline May 7, 2022: Full paper deadline June 15, 2022: Author notification June 26, 2022: Final version deadline (firm) PROGRAM COMMITTEE Arthur Azevedo de Amorim (Boston University) Agata Ciabattoni (Technische Universität Wien) (Co-Chair) Diana Costa (University of Lisbon) Denisa Diaconescu (University of Bucharest) Hans van Ditmarsch (Open University of the Netherlands) Rajeev Goré (The Australian National University) Roman Kuznets (Technische Universität Wien) João Marcos (Univ Federal do Rio Grande do Norte) Larry Moss (Indiana University Bloomington) Valeria de Paiva (Topos Institute and PUC-Rio) Elaine Pimentel (University College London) (Co-Chair) Revantha Ramanayake (University of Groningen) Mehrnoosh Sadrzadeh (University College London) Alexandra Silva (Cornell University) Alex Simpson (University of Ljubljana) Sonja Smets (University of Amsterdam) Alwen Tiu (The Australian National University) Leon van der Torre (University of Luxembourg) Andrea Aler Tubella (Umeå University) Andres Villaveces (Universidad Nacional de Colombia) Renata Wassermann (Universidade de São Paulo) STEERING COMMITTEE Samson Abramsky, Anuj Dawar, Juliette Kennedy, Ulrich Kohlenbach, Daniel Leivant, Leonid Libkin, Lawrence Moss, Luke Ong, Valeria de Paiva, Ruy de Queiroz, Alexandra Silva, Renata Wassermann. ADVISORY COMMITTEE Johan van Benthem, Joe Halpern, Wilfrid Hodges, Angus Macintyre, Hiroakira Ono, Jouko Väänänen. ORGANISING COMMITTEE Ștefan Ciobâcă (Alexandru Ioan Cuza Univ) (Co-Chair) Anjolina G. de Oliveira (Univ Federal de Pernambuco, Brasil) Ruy de Queiroz (Univ Federal de Pernambuco, Brasil) (co-chair) SCIENTIFIC SPONSORSHIP European Association for Computer Science Logic (EACSL) Interest Group in Pure and Applied Logics (IGPL) The Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) (tbc) European Association for Theoretical Computer Science (EATCS) (tbc) Sociedade Brasileira de Lógica (SBL) SPECIAL SESSION: SCREENING OF MOVIES ABOUT MATHEMATICIANS It is planned to have a special session with the exhibition of a one-hour documentary film about a remarkable mathematician who is considered a father of modern differential geometry. "Taking the Long View: The Life of Shiing-shen Chern" (George Scisery, 2011) examines the life of a remarkable mathematician whose formidable mathematical contributions were matched by an approach and vision that helped build bridges between China and the West. The biographical documentary follows Shiing-shen Chern (1911-2004) through many of the most dramatic events of the 20th century, portraying a man who dedicated his life to pure mathematics with the style of a classical Chinese sage. (zalafilms.com) FURTHER INFORMATION Contact one of the Co-Chairs of the Organising Committee. WEB PAGE https://wollic2022.github.io/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Reminder: PhD positions in Stockholm, deadline this Friday, 22 April
by Peter LeFanu Lumsdaine 19 Apr '22

19 Apr '22

Dear all, A reminder for all interested in the PhD openings here that the deadline is *this Friday*, 22 April (full information repeated below). (Note: if you’ve contacted me about this before last week and I haven’t replied yet, please write again — at least a couple of inquiries got caught in my spam filter, so it’s possible there are more I missed, for which my apologies! If you wrote last week, expect a reply today.) Best, –Peter. Dear all, We are recruiting for PhD students in HoTT (and other topics) at the Stockholm University Department of Mathematics, starting Autumn 2022. The deadline for applications is Friday, April 22. Full details and application are through the university website: https://www.su.se/english/about-the-university/work-at-su/available-jobs/ph… Please contact me if you have any questions about the position! And (for advisors) please pass this on to any interested masters-level students. Answers to a few common questions: - PhD positions in Sweden are fully funded, with a livable salary. - The position includes up to 20% teaching. - Swedish speaking isn’t required, either formally or practically (though learning it during the PhD is encouraged) — all higher-level teaching is done in English, and most administrative business (including all necessities) can be. Best wishes, –Peter. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Postdoc position in Tokyo: model checking and optimization metaheuristics
by Ichiro Hasuo 19 Apr '22

19 Apr '22

[Please distribute, apologies for multiple postings.] Open Position for a PostDoc Researcher (Model Checking Extended with Optimization Metaheuristics, April 2022) ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD <https://group-mmm.org/eratommsd/>) invites applications for a postdoc researcher. We aim to combine model checking and optimization metaheuristics, in order to scale formal verification techniques up to real-world industrial problems that are complex and black-box. We aim to do so, at the same time, in a way guided by solid meta-theoretical foundations such as those which we've presented in LICS and CAV. We thus explore new shapes of application of logic to modern software and systems. The position will be especially suited for those who have experience in model checking research and who wish to expand their research portfolio. Some further details are found below. See https://group-mmm.org/eratommsd/open-position-for-a-postdoc-researcher-marc… for full details. Thanks a lot for your consideration. Best, Ichiro ------------- JOB DESCRIPTION The candidate will work at National Institute of Informatics <https://www.nii.ac.jp/en/>, Tokyo, Japan, and will pursue a novel extension of model checking techniques (temporal logic, automata theory) with optimization metaheuristics (evolutionary computation, stochastic optimization, statistical machine learning). The goal is to overcome two major challenges that currently limit the applicability of formal verification techniques to real-world industrial systems, namely *scalability* and the *absence of white-box models*. In our endeavor towards the goal, we do not mind relying on testing, rather than exhaustive verification; this puts us somewhat closer to so-called *lightweight formal methods*. That said, our theoretical development shall be nothing "lightweight." We believe that there is a great theoretical depth here--we will explore the depth using logical, automata-theoretic, and/or categorical machinery. This *theory of * *"lightweight" formal methods* will significantly expand the current landscape of application of logic to software. The position should be especially suited for model checking researchers who wish to expand their research portfolio. We find case studies in our industrial collaborations and seek applicability to those real-world problems (they are mostly from the manufacturing industry). At the same time, we seek rigorous logical/automata-theoretic/categorical foundations for the solutions we come up with--so our work stays well in the realm of the formal verification community. We work in an interdisciplinary environment, and the candidate will be constantly exposed to interaction with control theory, software engineering, automated driving, and category theory. The candidate will work closely with Prof. Ichiro Hasuo <https://group-mmm.org/~ichiro/> and a few other team members. It is possible that the candidate be granted an academic title (such as Project Assistant/Associate Professor). References The following are some outcomes of our efforts so far. They are listed here in order to exemplify concrete topics. Note that the topics of these papers are diverse, and the candidate is not expected to follow all of them. A good match with one of them would suffice. - Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring Against Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi <https://doi.org/10.1007/978-3-030-25540-4_30> arXiv <https://arxiv.org/abs/1905.04486> (The topic is the theory of timed automata, which strikes a balance between theory and applicability.) - Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo: Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. CAV (2) 2020: 349-371 doi <https://link.springer.com/chapter/10.1007/978-3-030-53291-8_19> arXiv <https://arxiv.org/abs/2007.07421> (A work on a rather classic topic in formal verification, but the algorithm is approximate and highly scalable. The basic idea behind the algorithm has potential extensions, both theoretically and practically) - Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini: Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification. CAV (1) 2019: 401-420. doi <https://doi.org/10.1007/978-3-030-25540-4_23> arXiv <https://arxiv.org/abs/1905.07549> (The work exploits logical structures to organize optimization metaheuristics on continuous domains.) - Sota Sato, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo: Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case Study. FM 2021: 313-329. doi <https://doi.org/10.1007/978-3-030-90870-6_17> (A real-world case study of logically structured optimization metaheuristics) - Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, Ichiro Hasuo: Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation. LICS 2021: 1-14. doi <https://ieeexplore.ieee.org/document/9470656/> arXiv <https://arxiv.org/abs/2105.10164> (A categorical work, a potential foundation of our theory. If this paper is your closest match, please note that you are expected to be eager in working with optimization metaheuristics too.) - Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga, Ichiro Hasuo: The Lattice-Theoretic Essence of Property Directed Reachability Analysis. CoRR abs/2203.14261 (2022) arXiv <https://arxiv.org/abs/2203.14261> (Another categorical work, but with a big emphasis on implementation. You are expected to be familiar with or eager for both.) ====== Ichiro Hasuo Professor, National Institute of Informatics i.hasuo(a)acm.org Secretaries: hasuolab-secr(a)nii.ac.jp http://group-mmm.org/~ichiro/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0