February 2019 - Categories - categories.org.au

Funding available for Second School and Workshop on Univalent Mathematics, Birmingham (UK), April 1-5
by Marco Maggesi 01 Mar '19

01 Mar '19

Dear all, Funding is available for participation in the Second School and Workshop on Univalent Mathematics, to be held at the University of Birmingham (UK), April 1-5, 2019 (https://unimath.github.io/bham2019) Details of the event are given below. Participants ("trainees") eligible to be reimbursed: Trainees must be engaged in an official research programme as a PhD Student or postdoctoral fellow or can be employed by, or affiliated to, an institution, organisation or legal entity which has within its remit a clear association with performing research. Trainees eligible for reimbursement: 1. Trainees from COST Full Members / COST Cooperating Member. 2. Trainees from Approved NNC Institutions. 3. Trainees from Approved European RTD Organisations. COST member countries are listed on https://www.cost.eu/who-we-are/members/member-states-2/ The precise conditions for funding by COST are given in Section 6 of https://www.cost.eu/wp-content/uploads/2018/10/20180501-Vademecum2.pdf Overview ======== Homotopy Type Theory is an emerging field of mathematics that studies a fruitful relationship between homotopy theory and (dependent) type theory. This relation plays a crucial role in Voevodsky's program of Univalent Foundations, a new approach to foundations of mathematics based on ideas from homotopy theory, such as the Univalence Principle. The UniMath library is a large repository of computer-checked mathematics, developed from the univalent viewpoint. It is based on the computer proof assistant Coq. In this school and workshop, we aim to introduce newcomers to the ideas of Univalent Foundations and mathematics therein, and to formalizing mathematics in a computer proof assistant based on Univalent Foundations. Format ======= We will have two tracks: - Beginners track - Advanced track: suitable for participants with some experience in Univalent Foundations and the proof assistant Coq. In the beginners track, you will receive an introduction to Univalent Foundations and to mathematics in those foundations, by leading experts in the field. In the accompanying problem sessions, you will formalize pieces of univalent mathematics in the UniMath library. In the advanced track, you will work, in a small group, on formalizing a specific topic in UniMath, guided by an expert in univalent mathematics. Your code will become part of the UniMath library. Application and funding ======================= For information on how to participate, please visit https://unimath.github.io/bham2019. Funding will be given out on a `first come first served` basis. Related events =========== The 6th Workshop on Formal Topology (http://www.cs.bham.ac.uk/~sjv/6WFTop/) and the Midlands Graduate School (http://events.cs.bham.ac.uk/mgs2019/) are going to take place in the two weeks following the School and Workshop on Univalent Foundations. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ARRAY workshop at PLDI 2019, submissions due 8th April
by Jeremy Gibbons 26 Feb '19

26 Feb '19

CALL FOR PAPERS ARRAY 2019 6th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming co-located with PLDI 2019 at ACM FCRC 22nd June 2019, Phoenix, Arizona https://pldi19.sigplan.org/ ABOUT Array-oriented programming offers a unique blend of programmer productivity and high-performance parallel execution. As an abstraction, it directly mirrors high-level mathematical constructions commonly used in many fields from natural sciences over engineering to financial modelling. As a language feature, it exposes regular control flow, exhibits structured data dependencies, and lends itself to many types of program analysis. Furthermore, many modern computer architectures, particularly highly parallel architectures such as GPUs and FPGAs, lend themselves to efficiently executing array operations. This workshop is intended to bring together researchers from many different communities, including language designers, library developers, compiler researchers and practitioners who are using or working on numeric, array-centric aspects of programming languages, libraries and methodologies from all domains: imperative or declarative; object-oriented or functional; interpreted or compiled; strongly typed, weakly typed or untyped. TOPICS The ARRAY series of workshops explores: - formal semantics and design issues of array-oriented languages and libraries; - productivity and performance in compute-intensive application areas of array programming; - systematic notation for array programming, including axis- and index-based approaches; - intermediate languages, virtual machines, and program-transformation techniques for array programs; - representation of and automated reasoning about mathematical structure, such as static and dynamic sparsity, low-rank patterns, and hierarchies of these, with connections to applications such as graph processing, HPC, tensor computation and deep learning; - interfaces between array- and non-array code, including approaches for embedding array programs in general-purpose programming languages; and - efficient mapping of array programs, through compilers, libraries, and code generators, onto execution platforms, targeting multi-cores, SIMD devices, GPUs, distributed systems, and FPGA hardware, by fully automatic and user-assisted means. Array programming is at home in many communities, including language design, library development, optimization, scientific computing, and across many existing language communities. ARRAY is intended as a forum where these communities can exchange ideas on the construction of computational tools for manipulating arrays. IMPORTANT DATES Paper submissions: 8th April, 2019 (anywhere on earth) Notification of authors: 27th April, 2019 Camera-ready copies due: 10th May, 2019 Workshop date: 22nd June, 2019 SUBMISSIONS Submissions are welcome in two categories: full papers and extended abstracts. All submissions should be formatted in conformance with the ACM SIGPLAN proceedings style. Accepted submissions in either category will be presented at the workshop. Full papers may be up to 12pp, on any topic related to the focus of the workshop. They will be thoroughly reviewed according to the usual criteria of relevance, soundness, novelty, and significance; accepted submissions will be published in the ACM Digital Library. Extended abstracts may be up to 2pp; they may describe work in progress, tool demonstrations, and summaries of work published in full elsewhere. The focus of the extended abstract should be to explain why the proposed presentation will be of interest to the ARRAY audience. Submissions will be lightly reviewed only for relevance to the workshop, and will not published in the DL. Whether full papers or extended abstracts, submissions must be in PDF format, printable in black and white on US Letter sized paper. Papers must adhere to the standard SIGPLAN conference format: two columns, nine-point font on a ten-point baseline, with columns 20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc (0.33in). A suitable document template for LaTeX is available at http://www.sigplan.org/Resources/Author/. Papers must be submitted using EasyChair: https://easychair.org/conferences/?conf=array2019. AUTHORS TAKE NOTE: The official publication date of full papers is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the workshop. The official publication date affects the deadline for any patent filings related to published work. ORGANIZING COMMITTEE Jeremy Gibbons, University of Oxford, UK (chair) PROGRAMME COMMITTEE Paolo Bientinesi, Umeå University, SE Christophe Dubach, University of Edinburgh, UK Vinod Grover, NVIDIA, US Magne Haveraaen, University of Bergen, NO Troels Henriksen, University of Copenhagen, DK Tze Meng Low, Carnegie-Mellon University, US Hidehiko Masuhara, Tokyo Institute of Technology, JP Trevor L. McDonell, Utrecht University, NL Lenore Mullin, SUNY Albany, US Tatiana Shpeisman, Google Brain, US ARRAY 2018 is sponsored by ACM SIGPLAN. Student presenters of accepted submissions are eligible to apply to the SIGPLAN PAC (http://sigplan.org/PAC/) for travel funding. Jeremy.Gibbons(a)cs.ox.ac.uk Oxford University Department of Computer Science, Wolfson Building, Parks Road, Oxford OX1 3QD, UK. ☎ +44 1865 283521 http://www.cs.ox.ac.uk/people/jeremy.gibbons/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

John Gray
by Michael＠mathstat.dal.ca 26 Feb '19

26 Feb '19

------------------------------------ From: Michael Barr, Prof. <barr.michael(a)mcgill.ca> Sent: February 25, 2019 11:24 To: Bob Rosebrugh Subject: John Gray I don't know if the cat list ever posted anything about John Gray's death. Here is something a friend in Urbana sent me when I asked about John (whom I hadn't heard from in years and wondered about) written by one of his sons. If you think it appropriate, you could send to the list. Mike ---------------------------------------------- John Gray URBANA - John Walker Gray died May 17, 2017, at age 85. It was not unexpected. He died as he lived, in a comfortable and well-planned manner, his needs anticipated, and care taken that his affairs be in order. He was there for my first breath, and I was there for his last, as is good and right. His foresight gave him, at the end of his time, an interval of rest and contentment that all deserve, but few are afforded. Born to a merchant, he imagined for himself a life of the mind. Through hard work and patient dedication, he made that a reality, becoming an erudite and well-traveled man, a talented pianist and a mathematician of note in several fields. The arc of his life was a work of his own devising, and it was good. John went from an undergraduate degree from Swarthmore College in 1953 to his doctorate from Stanford University in 1957 as a student of the renowned Charles Loewner. His doctoral thesis on contact structures, published in the Annals of Mathematics, remains of interest today, having been cited nearly a hundred times in recent years alone. As a professor of mathematics at the University of Illinois, John supervised five Ph.D. students and at the end of his career served as director of graduate studies. His research interests centered on category yheory, a study of patterns common to many parts of mathematics including algebra, topology, logic and computer science. His 1974 book on formal category theory has long been a standard reference. John contributed to categorical semantics of programming languages, including versions of the lambda calculus, and he attracted several of the founders and early employees of Wolfram Research to Urbana. He made his mark, advanced the art, and his students take a part of him into the future. John was preceded in death by his wife of many years, Eva Wirth Gray, who introduced him to Switzerland where he spent happy sabbatical years and where his only daughter, Elizabeth, died at age 15. Of his siblings, Corinne, Suzanne and Nancy, only the last survives him, as do his nephews Allen, Tom and Kayvon. Yiling, Laur and Tony preceded him in death. Of his own, he is survived by his sons, Stephen and Theodore; and three grandchildren, Addie, Emma and Connor. He is also survived by all but one of a dedicated group of caregivers who became his second family late in life. To this family - Brittany, Mary, Jan, Ashley and the tragically departed Tiffany - his first family extends their most heartfelt thanks for the love and care he received right up until the last moment of his life. John Walker Gray executed the story of his life well and completed it with grace. He will be missed by all who knew him. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

large integrals via manageable ends?
by rjwood＠mathstat.dal.ca 24 Feb '19

24 Feb '19

With reference to the following diagram in \CAT, where \set is the category of small sets: F \A------->\B | P| | v \set it is classical that if \A is small and \B is locally small then the left Kan extension of P along F exists, call it L, and for B in \B LB=\int^A \B(FA,B) x PA. Clearly, local smallness of B can be weakened to the requirement that all \B(FA,B) are small, a condition called `admissibility' of F, by Street and Walters in their `Yoneda structures' paper. The point is that a small integral of small sets is small. However, I claim that smallness of \A can be `weakened' to local smallness of \set^{\A\op}. If we include \set in a category \SET of sets large enough to contain all the LB as above, via I:\set----->\SET then the description of L also gives a left Kan extension of IP along F. Now write p(LB) for the power set of LB and consider the following calculation: p(LB)=\SET(\int^A \B(FA,B) x PA, 2)=\int_A\SET(\B(FA,B), 2^{PA}) =\int_A\set(\B(FA,B), 2^{PA}) =\set^{\A\op}(\B(F-,B),\set(P-,2)) It shows that local smallness of \set^{\A\op} implies p(LB) is small and hence that LB is small. Thus for \set^{\A\op} locally small and F admissible, the left Kan extension of any P:\A--->\set along F exists and is given by the usual formula. This calculation was prompted by questions similar to an open problem in the paper by Freyd and Street `On the size of categories' in TAC V1. Can anybody provide pointers to similar calculations where a big integral is tamed by a manageable end? Thanks, RJ Wood [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

NLCS 2019, Gothenburg, as part of IWCS2019
by Valeria de Paiva 23 Feb '19

23 Feb '19

Sixth Workshop on Natural Language and Computer Science NLCS '19 May 24, 2019 Gothenburg, Sweden http://www.indiana.edu/~iulg/nlcs.html A workshop affiliated with the 13th International Conference on Computational Semantics (IWCS 2019) https://sites.google.com/view/iwcs2019/ Endorsed by the Association for Computational Linguistics Special Interest Group on Computational Semantics. AIMS AND SCOPE Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. Specific topics includes, but are not limited to: * logic for semantics of lexical items, sentences, discourse and dialog * continuations in natural language semantics * formal tools in textual inference, such as logics for natural language inference * applications of category theory in semantics * linear logic in semantics * formal approaches to unifying data-driven and declarative approaches to semantics INVITED SPEAKERS Krasimir Angelov, University of Gothenburg Rafaella Bernardi, University of Trento PROGRAM COMMITTEE Robin Cooper, University of Gothenburg Valeria de Paiva, Nuance Daisuke Bekki, Ochanomizu University Dag Haug, University of Oslo Aurelie Herbelot, University of Trento Makoto Kanazawa, Hosei University Larry Moss, Indiana University, Bloomington Gerald Penn, University of Toronto Adam Przepiorkowski, Institute of Computer Science, Polish Academy of Sciences Kyle Richardson, Allen Institute for Artificial Intelligence PAPER SUBMISSIONS Extended abstracts of up to 10 pages may be submitted through Easychair: https://easychair.org/conferences/?conf=nlcs18 ORGANIZERS Robin Cooper, University of Gothenburg Email: robin.cooper at ling. gu. se Valeria de Paiva Nuance Email: Valeria.dePaiva at gmail .com Larry Moss Indiana University Email: lsm at cs.indiana . edu IMPORTANT DATES Registration of abstracts: March 1 Paper submission: March 7 Notification: April 7 Electronic versions due: April 20 Workshop Date: May 24, 2019 IWCS'19 Dates: 23-27th May 2019 -- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Terminology regarding injectivity of objects
by Martin Escardo 23 Feb '19

23 Feb '19

On 09/02/2019 21:43, ptj(a)maths.cam.ac.uk wrote: > I encountered this situation when I considered injectivity in Top: > see my paper in SLNM 871, and also pages 738-9 in?? the Elephant. > I used the terms `weakly injective' and `strongly injective' (not > very imaginative, but they did the job), and also `completely > injective' for the case where the `extension along j' operation can be > taken to be right adjoint to restriction along j (you could of > course use `cocompletely injective' for the case where it's left adjoint). > Fortunately, in Top the notions of weak injective, strong injective > and complete injective coincide. The paper John Bourke, 2017, Equipping weak equivalences with algebraic structure. https://arxiv.org/abs/1712.02523. has a terminology for this that is appealing: an algebraic injective object, with respect to a class J of arrows, is an object D equipped with extensions c(j,f) : Y -> D for each j:X->Y in J and f : X -> D. (Then you can consider the obvious morphisms of algebraic injective objects that commute with the designated extensions c(j,f).) Thanks to Mike Shulman for this reference. Martin > > Peter Johnstone > > On Feb 9 2019, Mart??n H??tzel Escard?? wrote: > >> >> (1) An object D is called injective over an arrow j:X->Y if the >> "restriction map" >> >> ???????? hom(Y,D) -> hom(X,D) >> ???????????????? g???? |-> g o j >> >> is a surjection. This is fairly standard terminology (where does it come >> from, by the way). >> >> (2) I am working with the situation where the restriction map is a >> *split* surjection. >> >> I though of the terminology "D is split injective over j", but perhaps >> this is awkward. Is there a standard terminology for this notion. Or, >> failing that, a terminology that at least one person has already used in >> the literature or in the folklore. Or, failing that too, a good >> suggestion by any of you? >> >> Thanks, >> Martin >> >> >> [For admin and other information see: http://www.mta.ca/~cat-dist/ ] >> > -- Martin Escardo http://www.cs.bham.ac.uk/~mhe [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

LCC 2019: Call for Contributions
by anupamdotdas＠gmail.com 22 Feb '19

22 Feb '19

=========================================================== First Call for Contributions LCC 2019 20th International Workshop on Logic and Computational Complexity July 8, 2019, Patras, Greece Collocated with ICALP 2019 http://www.cs.swansea.ac.uk/lcc/ =========================================================== LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. IMPORTANT DATES: * submission May 1, 2019 * notification May 20, 2019 * workshop July 8, 2019 SUBMISSION: Submissions must be in English and in the form of an abstract of about 3-4 pages. All submissions should be submitted through Easychair at: https://easychair.org/conferences/?conf=lcc19 We also welcome submissions of abstracts based on work submitted or published elsewhere, provided that all pertinent information is disclosed at submission time. There will be no formal reviewing as is usually understood in peer-reviewed conferences with published proceedings. The program committee checks relevance and may provide additional feedback. PROGRAM COMMITTEE: Lauri Hella, Co-chair, Tampere University, Finland Monika Seisenberger, Co-chair, Swansea University, UK Sam Buss, University of California, San Diego, US Anupam Das, University of Copenhagen, Denmark Anuj, Dawar, University of Cambridge, UK Akitoshi Kawamura, Kyushu University, Fukuoka, Japan Arne, Meier, University of Hannover, Germany Lidia Tendera, University of Opole, Poland CONTACT: To contact the workshop organizers, please send an e-mail to lcc19(a)easychair.org [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Quantum Physics and Logic 2019: CALL FOR PAPERS
by Bob Coecke 22 Feb '19

22 Feb '19

CALL FOR PAPERS 16th International Conference on Quantum Physics and Logic (QPL 2019) June 10-14, 2019 Chapman University, Orange, California, USA https://qpl2019.org <https://qpl2019.org/> * * * The 16th International Conference on Quantum Physics and Logic (QPL 2019) will take place at Chapman University June 10-14, 2019. The conference brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general. Work that applies structures and methods inspired by quantum theory to other fields (including computer science) is also welcome. IMPORTANT DATES April 1: abstract submission April 7: paper submission April 30: application for student support May 12: notification of authors May 17: early registration deadline May 24: final papers ready June 10-14: conference INVITED SPEAKERS John Baez (UC Riverside) Anna Pappa (University College London) Joel Wallman (University of Waterloo) INVITED TUTORIALS Ana Belen Sainz (Perimeter Institute) Quanlong Wang (University of Oxford) SUBMISSIONS Prospective speakers are invited to submit one (or more) of the following: - Original contributions consist of a 5-12 page extended abstract that provides sufficient evidence of results of genuine interest and enough detail to allow the program committee to assess the merits of the work. Submission of substantial albeit partial results of work in progress is encouraged. - Extended abstracts describing work submitted/published elsewhere will also be considered, provided the work is recent and relevant to the conference. These consist of a 3 page description and should include a link to a separate published paper or preprint. The conference proceedings will be published in Electronic Proceedings in Theoretical Computer Science (EPTCS) after the conference. Only "original contributions" are eligible to be published in the proceedings. Submissions should be prepared using LaTeX, and must be submitted in PDF format. Use of the EPTCS style is encouraged. Submission is done via EasyChair: https://www.easychair.org/conferences/?conf=qpl2019 <https://www.easychair.org/conferences/?conf=qpl2019> There will be an award for the best student paper at the discretion of the programme committee. Papers eligible for the award are those where all the authors are students at the time of submission. PROGRAM COMMITTEE Bob Coecke (co-chair, University of Oxford) Matthew Leifer (co-chair, Chapman University) Miriam Backens (University of Oxford) Giulio Chiribella (University of Oxford) Stefano Gogioso (University of Oxford) John Harding (New Mexico State University) Chris Heunen (The University of Edinburgh) Matthew Hoban (University of Oxford) Dominic Horsman (University of Durham) Kohei Kishida (Dalhousie University) Aleks Kissinger (Radboud University) Joachim Kock (UAB) Ravi Kunjwal (Perimeter Institute for Theoretical Physics) Martha Lewis (University of Amsterdam) Dan Marsden (University of Oxford) David Moore (Pictet Asset Management) Michael Moortgat (Utrecht University) Daniel Oi (University of Strathclyde) Ognyan Oreshkov (Université Libre de Bruxelles) Anna Pappa (University College London) Dusko Pavlovic (University of Hawaii) Simon Perdrix (CNRS, Laboratoire d'Informatique de Grenoble, University of Grenoble) Neil Ross (Dalhousie University) Mehrnoosh Sadrzadeh (Queen Mary University of London) Ana Belén Sainz (Perimeter Institute for Theoretical Physics) Peter Selinger (Dalhousie University) Sonja Smets (University of Amsterdam) Pawel Sobocinski (University of Southampton) Robert Spekkens (Perimeter Institute for Theoretical Physics) Isar Stubbe (Université du Littoral) Benoît Valiron (LRI - CentraleSupelec, Univ. Paris Saclay) Jamie Vicary (University of Oxford) Alexander Wilce (Susquehanna University) Mingsheng Ying (University of Technology, Sydney) Margherita Zorzi (University of Verona) Magdalena Anna Zych (The University of Queensland) STEERING COMMITTEE Bob Coecke (University of Oxford) Prakash Panangaden (McGill University) Peter Selinger (Dalhousie University) LOCAL ORGANIZERS Lorenzo Catani (Chapman University) Justin Dressel (Chapman University) Matthew Leifer (Chapman University) Drew Moshier (Chapman University) For further information, please contact qpl2019(a)easychair.org <mailto:qpl2019@easychair.org>. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Proof-Theoretic Semantics, Tuebingen, 27-30 March 2019
by Peter Schroeder-Heister 22 Feb '19

22 Feb '19

Proof-Theoretic Semantics: Assessment and Future Perspectives Third Tübingen Conference on Proof-Theoretic Semantics 27–30 March 2019 in Tübingen, Germany http://ls.informatik.uni-tuebingen.de/PTS3/ Call for participation If you would like to attend the conference, please send an email to Marine Gaudefroy-Bergmann at pts3part(a)informatik.uni-tuebingen.de by March 18. Plenary speakers are: - Vito Michele Abrusci (Roma) - Patrizio Contu (Zürich) - Valeria de Paiva (Cupertino) - Marie Duzi (Ostrava) - Nissim Francez (Haifa) - Andrzej Indrzejczak (Lodz) - Gerhard Jäger (Bern) - Reinhard Kahle (Lisbon/Tübingen) - Per Martin-Löf (Stockholm) - Dale Miller (Palaiseau) - Sara Negri (Helsinki) - Luiz Carlos Pereira (Rio de Janeiro) - Francesca Poggiolesi (Paris) - Dag Prawitz (Stockholm) - David Pym (London) - Greg Restall (Melbourne) - Peter Schroeder-Heister (Tübingen) - Phil Scott (Ottawa) - Göran Sundholm (Leiden) - Heinrich Wansing (Bochum) For the list of contributing speakers see http://ls.informatik.uni-tuebingen.de/PTS3/contributed.html. There will be a small conference fee covering coffee breaks. Organisers: Thomas Piecha and Peter Schroeder-Heister -- Prof. Peter Schroeder-Heister Department of Computer Science University of Tuebingen Sand 13 72076 Tuebingen Germany Phone: +49-7071-2974284 (secr. -2978958) Fax: +49-7071-295060 e-mail: psh(a)uni-tuebingen.de http://ls.inf.uni-tuebingen.de [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

TYPES 2019, 11-14 June 2019, Oslo: Announcement and final call for contributions, DEADLINE 4 MARCH
by Marc.Bezem＠uib.no 18 Feb '19

18 Feb '19

ANNOUNCEMENT AND FINAL CALL FOR CONTRIBUTIONS (DEADLINE 4 MARCH) 25th International Conference on Types for Proofs and Programs, TYPES 2019 and EUTYPES Cost Action CA15123 meeting Oslo, Norway, 11 - 14 June 2019 https://cas.oslo.no/types2019/ TYPES 2019 will be held in parallel (and jointly on 12 June) with HoTT-UF, 12-14 June 2019, https://cas.oslo.no/hott-uf/ BACKGROUND The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. The EUTypes Cost Action CA15123 (eutypes.cs.ru.nl) focuses on the same research topics as TYPES and partially sponsors the TYPES Conference: Part of the programme is organised under the auspices of EUTypes. INVITED SPEAKERS * Adam Chlipala (MIT, Cambridge MA, USA) * Assia Mahboubi, (INRIA, Nantes, France) * Conor McBride (University of Strathclyde, Glasgow, UK) * Stephanie Weirich (University of Pennsylvania, Pittsburgh, USA) CONTRIBUTED TALKS We solicit contributed talks: https://cas.oslo.no/types2019/submission/ Selection of those will be based on extended abstracts/short papers of 2 pp formatted with easychair.cls. The submission site is https://easychair.org/conferences/?conf=types2019 Important dates: * submission of 2 pp abstract: Monday 4 March 2019, anywhere on Earth * notification of acceptance/rejection: 15 April 2019 * camera-ready version of abstract: 6 May 2019 Camera-ready versions of the accepted contributions will be published in an informal book of abstracts for distribution at the workshop. POST-PROCEEDINGS Similarly to TYPES 2011 and TYPES 2013-2018, a post-proceedings volume will be published in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to that volume will be open to everyone. Tentative submission deadline for the post-proceedings: September 2019. PROGRAMME COMMITTEE Thorsten Altenkirch (University of Nottingham) Marc Bezem (University of Bergen, chair) Małgorzata Biernacka (University of Wrocław) Jesper Cockx (Chalmers University Gothenburg) Herman Geuvers (Radboud University Nijmegen) Silvia Ghilezan (University of Novi Sad) Mauro Jaskelioff (Universidad Nacional de Rosario) Ambrus Kaposi (Eötvös Loránd University) Ralph Matthes (IRIT - CNRS and University of Toulouse) Étienne Miquey (INRIA, France) Leonardo da Moura (Microsoft Research) Keiko Nakata (SAP Potsdam) Fredrik Nordvall Forsberg (University of Strathclyde) Benjamin Pierce (University of Pennsylvania) Elaine Pimentel (Federal University of Rio Grande do Norte) Luís Pinto (University of Minho) Simona Ronchi Della Rocca (Università di Torino) Carsten Schürmann (IT University of Copenhagen) Wouter Swierstra (Utrecht University) Tarmo Uustalu (Reykjavik University) TYPES STEERING COMMITTEE Andreas Abel, Marc Bezem, José Espírito Santo, Hugo Herbelin, Ambrus Kaposi, Ralph Matthes (chair). ABOUT TYPES The TYPES meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. From 2009 to 2015, TYPES has been run as an independent conference series. From 2016, TYPES is partially supported by COST Action EUTypes CA15123. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016), Budapest (2017), Braga (2018). CONTACT Email: types2019 at cas.oslo.no Organisers: Marc Bezem (University of Bergen, chair) Bjørn Ian Dundas (University of Bergen) Erna Kas (Utrecht University) Camilla K. Elmar (Centre for Advanced Study) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0