January 2014 - Categories - categories.org.au

Partial functor
by David Leduc 16 Mar '15

16 Mar '15

Hi, A partial functor from C to D is given by a subcategory S of C and a functor from S to D. What is the appropriate notion of natural transformation between partial functors that would allow to turn small categories, partial functors and those "natural transformations" into a bicategory? The difficulty is that two partial functors from C to D might not have the same definition domain. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 6

Research positions
by Maria Manuel Clementino 26 Feb '14

26 Feb '14

5-YEAR RESEARCH POSITIONS The Centre for Mathematics of the University of Coimbra (CMUC) invites applications for five 5-year research positions in all areas of Mathematics. Applicants should have a PhD in Mathematics and at least three years of post-doctoral experience, with an international-level publication record and demonstrated ability to perform independent research. Preference will be given to candidates working in one of the areas in which the members of CMUC are currently active. A very good command of English is required. The appointments will be made for three years, renewable for two more. Successful applicants are expected to develop research within the areas of interest of CMUC. They should also contribute to graduate studies, supervising students from the Department of Mathematics. The basic salary is equivalent to the index 195 of the Portuguese research career (in the order of 42 500 euros a year), in accordance with the Ciência 2008 guidelines http://alfa.fct.mctes.pt/apoios/contratacaodoutorados/edital2008 Benefits include private health insurance and social security. Applicants should send • cover sheet (available from www.mat.uc.pt/cmuc/coversheet.pdf) including names and contact information of three persons who can provide a letter of recommendation • curriculum vitae (publication list included) • a 5-year research proposal (2 pages max), emphasizing their own research goals as pdf files to cmuc(a)mat.uc.pt. The subject of the e-mail message must include the job reference C2008 FCTUC CMUC v15-v19. The deadline for applications is *September 10, 2008.* ------------------------------ More information can be found at www.mat.uc.pt

1 1

Correctness by Construction, Genoa, Italy, 24-27 March 2014
by Eugenio Moggi 30 Jan '14

30 Jan '14

_________________________________________________________________________ Correctness by Construction, Workshop, Genoa, Italy, 24-27 March 2014 http://corcon2014.net/ _________________________________________________________________________ Correctness by Construction (CORCON) is an FP7 EU-funded project under the Marie Curie IRSES scheme. This kick-off workshop of CORCON aims at bringing together the participants of the project and those researchers who are interested in the themes of the project. The workshop is further promoted by AILA (Associazione Italiana di Logica e sue Applicazioni) and by the research project Logical Methods of Information Management. Themes of the Project (non-exclusive) Proof Theory, Type Theory and Constructive Set Theory Constructive Topology and Analysis Homotopy Type Theory Categorical Logic Programming Languages for Correct by Construction Programming Correct by Construction Programs over Continuous Data Correct by Construction Programs with Limited Resources Keynote Speakers (preliminary list) Marco Benini (University of Insubria) Hannes Diener (University of Siegen/University of Canterbury) Neil Ghani (University of Strathclyde) Hajime Ishihara (JAIST, Japan) Gyesik Lee (HNU, Korea) Maria Emilia Maietti (University of Padua) Eugenio Moggi (University of Genoa) Mizuhito Ogawa (JAIST, Japan) Erik Palmgren (Stockholm University) John Stell (University of Leeds) Michael Rathjen (University of Leeds) Giuseppe Rosolini (University of Genoa) Giovanni Sambin (University of Padua) Helmut Schwichtenberg (University of Munich) Monika Seisenberger (Swansea University) Dieter Spreen (University of Siegen) Satoshi Tojo (JAIST, Japan) Hideki Tsuiki (Kyoto University) Contributed Talks Abstracts in PDF, at most one page including references, can only be submitted via: https://www.easychair.org/conferences/?conf=corcon2014 In addition to contributions from members of the project sites, there will also be room for a few contributions by people from outside the project. Important Deadlines 13 February 2014 Abstracts of Contributed Papers 20 February 2014 Notification of Acceptance 27 February 2014 Early Registration: Reduced Fee 13 March 2014 Registration Closed More details, including information about registration, travel and accommodation, are or will be available on the project web page: http://corcon2014.net/ _________________________________________________________________________ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

postdoc offer in Paris
by Pierre-Louis Curien 27 Jan '14

27 Jan '14

One postdoc position is available in the ANR-NSFC project LOCALI * Location: Preuves, Programmes et Systemes laboratory (PPS) University Paris Diderot - Paris 7 * Description: http://www.pps.univ-paris-diderot.fr/postdoc-locali This is a pure research position without teaching duties, open to young researchers owning a PhD degree. The scientific activity will take place within the LOCALI French-Chinese ANR-NSFC project. The candidate is expected to submit a research project connected to at least one of the following topics: - operational and denotational semantics of functional languages and their extensions - Linear Logic and its extensions - Process Algebras, logics of processes, co-inductive techniques - algebraic and topological methods in Rewriting Theory or Type Theory. * Local project members The local members of the project LOCALI are: Antonio Bucciarelli, Pierre-Louis Curien and Thomas Ehrhard. They will be the main interlocutors of the recruited postdoctoral researcher. * Important dates: Duration: one year Starting date: between September 1st and December 31st, 2014 Application deadline: February 28th, 2014 Notification: before March 31st, 2014 * Salary: Take-home pay is around 2000 Euro per month. * Application: Please send, before the application deadline, the following documents: - CV - publication list - description of past research activities - postdoctoral research project - supporting letters (not mandatory) by email (PDF files) to the following address: postdoc-locali(a)pps.univ-paris-diderot.fr Description of the projet LOCALI: http://www.agence-nationale-recherche.fr/projet-anr/?tx_lwmsuivibilan_pi2[C… [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Joint 25th RTA & 12th TLCA: Last reminder
by Luca 25 Jan '14

25 Jan '14

Joint 25th International Conference on REWRITING TECHNIQUES AND APPLICATIONS and 12th International Conference on TYPED LAMBDA CALCULI AND APPLICATIONS July 14???17, 2014, Vienna, Austria http://vsl2014.at/rta-tlca ====================================== IMPORTANT DATES Abstract submission: January 28, 2014 Paper submission: February 4, 2014 Notification: April 9, 2014 Final version: April 29, 2014 Rebuttal period: March 19???21, 2014 ====================================== More info at: https://who.rocq.inria.fr/Gilles.Dowek/rta-tlca.html SUBMISSION and PUBLICATION --------------------------- Submissions presenting original work are expected at https://www.easychair.org/conferences/?conf=rtatlca2014. They should be at most 15 pages (10 for system descriptions) and follow http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0. The proceedings will be published in the LNCS Advanced Research in Computing and Software Science series of Springer. One author of each accepted paper is expected to present it at the conference. Topics ------ This joint RTA and TLCA conference is the major forum for the presentation of research on all aspects of rewriting and typed lambda-calculi. Areas of interest include but are not limited to: - Foundations: string rewriting; term rewriting; graph rewriting; lambdacalculi; higher-order rewriting; binding techniques; constrained rewriting and deduction; categorical and infinitary rewriting; stochastic rewriting; net rewriting; Petri nets; higher-dimensional rewriting; process calculi; explicit substitution; tree automata; confluence; termination; complexity; modularity. - Algorithmic aspects and implementation: strategies; matching; unification; anti-unification; narrowing; constraint solving; theorem proving; completion techniques; implementation techniques; parallel execution; certification of rewriting properties; abstract machines; automated (non)termination and confluence provers; automated complexity analysis; SMT solving; system descriptions. - Logic: proof theory; natural deduction; sequent calculi; proof assistants; cut elimination and normalization; propositions as types; linear logic and proof nets; equational logic; rewriting logic; rewriting calculi; proof checking; reasoning about programming languages and logics; homotopy type theory; type-theoretic aspects of complexity; implicit computational complexity. - Types: dependent types; polymorphism; intersection types and related approaches; subtyping; type inference and type checking; types in databases. - Semantics: denotational semantics; operational semantics; game semantics; realisability; domain theory; categorical models; universal algebra. - Programming: foundational aspects of functional programming, object oriented programming, and other programming paradigms; flow analysis of higher-type computation; program equivalence; program transformation; program optimization; program refactoring; rewriting models of programs; rule-based (functional and logic) programming; control operators; symbolic and algebraic computation; system synthesis and verification; XML queries and transformations; types in program analysis and verification; analysis of cryptographic protocols; systems biology; linguistics. Programme Committee -------------------- Andreas Abel (Gothenburg) Beniamino Accattoli (Bologna) Zena Ariola (Oregon) Steffen van Bakel (Imperial College) Pierre Clairambault (CNRS) Ugo Dal Lago (Bologna) Gilles Dowek (Inria) Santiago Escobar (Valencia) Amy Felty (Ottawa) Maribel Fernandez (King???s college) Adria Gascon (SRI International) Jeroen Ketema (Imperial College) Christopher Lynch (Clarkson) Masahito Hasegawa (Kyoto) Olivier Hermant (MINES ParisTech) Paul-Andre Mellies (CNRS) Alexandre Miquel (UdelaR) Cesar Munoz (NASA) Vivek Nigam (Para??ba) Luke Ong (Oxford) Brigitte Pientka (McGill) Femke van Raamsdonk (Amsterdam) Jakob Rehof (Dortmund) David Sabel (Frankfurt) Gernot Salzer (Wien) Sylvain Salvati (Inria) Aleksy Schubert (Warszawa) Peter Selinger (Dalhousie) Paula Severi (Leicester) Christian Sternagel (JAIST) Kazushige Terui (Kyoto) Mateu Villaret (Girona) Fer-Jan de Vries (Leicester) Harald Zankl (Innsbruck) Programme Chair --------------- Gilles Dowek Conference Chair ---------------- Gernot Salzer =============================================================== Luca Paolini, Sophie Tison RTA & TLCA publicity chairs [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Postdoc and PhD Positions at Regensburg
by Thomas Nikolaus 24 Jan '14

24 Jan '14

There is a new collaborative research center (SFB) "Higher Invariants - Interations between Arithmetic Geometry and Global Analysis" at the Department of Mathematics in Regensburg (Germany) starting April 1st. http://www.sfb-higher-invariants.de The CRC offers 10 Postdoc and 7 PhD Positions in various areas. We highly welcome applications (also as guests for shorter periods). We in particular announce the PhD Position in the project on T-Duality (U. Bunke, T. Nikolaus). This position comes without teaching obligation and a decent salary (3/4 of E13, roughly 1850 Euro/month after tax and healthcare deductions). We are seeking to hire a candidate interested in one of the following fields: - T-Duality and Mirror Symmetry - Generalized complex geometry - Homotopy theory and higher categories For application details and any further questions, please contact Thomas1.Nikolaus(a)mathematik.uni-regensburg.de [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Evaluation of source code, category theoretically?
by Mike Stay 23 Jan '14

23 Jan '14

What's the right way to think about evaluation in category theory? I'm guessing it will look kind of like this: the category will be symmetric monoidal closed and equipped with an object S whose points are "source code", together with a collection of interpreter epimorphisms run_{X, Y}: S -> [X, Y] and some notion of composition in S that works well with composition of morphisms. What are the right keywords for doing a literature search on this? -- Mike Stay - metaweta(a)gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 3

postdoc position in Toulouse on lightweight formal architecture specification
by David CHEMOUIL 21 Jan '14

21 Jan '14

Dear colleagues, A post-doctoral position is available in Toulouse, France, jointly proposed by Onera/DTIM and IRIT. Keywords: Formal specification, formal verification, lightweight formal methods, software architecture. PDF version here: <http://www.onera.fr/sites/default/files/u491/20140121-postdoc-formal-spec-a…> Location : Toulouse, France Onera supervisors : Julien Brunel & David Chemouil --> Mail: firstname.lastname(a)onera.fr IRIT supervisor: Jean-Paul Bodeveix --> Mail: lastname(a)irit.fr Subject ======= This subject fits into a joint research effort by Onera/DTIM and IRIT to devise lightweight formal methods for the specification and verification of dynamic software architecture. Architecture describes a system in terms of abstract concepts (e.g., components, connectors, configurations, behaviour contracts) and addresses extra-functional properties, while still enabling to draw a correspondence with higher-level requirements. Architecture Description Languages (ADLs) provide views focused on expressing the structure and the behaviour of a system as a composition of components and connectors. The formal specification and verification of behavioural properties of components and/or connectors have mainly been addressed using process-algebraic techniques (e.g., CSP for Wright , the \pi-calculus for Darwin ) or automata (e.g., constraint automata for coordination in Reo , various contract theories ). Finally, CommUnity is a notable approach relying on categorical methods to give an abstract account of various architectural concepts. Nevertheless, although studied in some works, some interesting questions, such as that of a more abstract specification language or that of formal refinement, have not been developed as thoroughly as in formal specification and lack tool support. Formal specification methods, indeed, such as Z , B (and more recently Event-B ) or VDM , often adopt a more abstract view than the ones cited above. These methods rely on expressive logics and promote formal refinement techniques. However, they are not very well suited to addressing architecture concerns as architectural elements (e.g., component and connector instances) are not first-class concepts. Furthermore, formal verification can only be partially automated because of the very expressiveness of the underlying logics. This last remark led to the development of Alloy which trades some expressiveness in favor of automated bounded verification based on SAT techniques. This approach, dubbed lightweight by its author as it promotes ???agility??? (quickly-available feedback of automated verification of small models) over the exhaustivity of more traditional formal methods, is surprisingly efficient in practice. Indeed, even if the verification is not complete, many intricate errors can be spotted for a relatively low modelling and verification effort. Nevertheless, as of now, Alloy does not feature first-class concepts to model behaviour nor architectural concerns (although some propositions exist, in particular for the former aspect). In this context, Onera/DTIM and IRIT are investigating the development of a lightweight formal specification approach for (possibly real-time) software architecture. The aim is thus to allow the ???declarative??? specification of behavioural and architectural concerns and the automated verification thereof. The present postdoctoral position takes place in this setting. Applicants should (be about to) hold a PhD in formal methods or theoretical computer science and should be willing to participate actively in the objective sketched above. The exact contribution will depend on the retained candidate and we are open to suggestions. For example (this is only indicative!), one may think of: - devising a new temporal logic providing a formal basis for the method - providing a formal semantics to the specification language - devising a categorical framework to account for composition or behaviour - developing SMT-based (SAT modulo theories) verification techniques (e.g., to address real-time aspects)??? Application =========== - Applicants should send a resume via email to David Chemouil and Jean-Paul Bodeveix. - Applicants are expected to be fluent in English or in French (possibility of French courses). - Position duration: 1 year. - Gross salary: ~2,500 ???/month (position funded by RTRA STAE, a French science foundation for space and aeronautics research). [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

1 year post-doctoral fellowship in Padova
by Maria Emilia Maietti 20 Jan '14

20 Jan '14

Dear colleagues, Applications are invited for a 12-months postdoctoral position in Mathematical Logic at the Department of Mathematics of the University of Padua, Italy. The call is aimed at researchers holding a PhD degree (or a comparable research activity). The title of the project is "From Constructive Mathematics to Foundations: models of type theory in the Basic Picture'' and it will be supervised by Prof. Giovanni Sambin. All applications in the area of Mathematical Logic will be considered. However, preference will be given to those candidates with some experience in constructive methods in mathematics. The salary is about 1500 euros per month. The applications should be sent before February 10, 2014. For further information, please visit: http://www.math.unipd.it/it/news/?id=1435 (in ITALIAN! Please contact us by e-mail if you don't read Italian). We encourage all applicants to contact us in advance for more specific information on the expected research topic. Note that the applications should be sent by registered mail (with "return receipt requested") to the address of the department. It is also possible to use "certified e-mail". Best regards, Francesco Ciraulo Milly Maietti Giovanni Sambin E-mails: {ciraulo, maietti, sambin} AT math.unipd.it [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Formalizations of category theory in proof assistants?
by Jason Gross 19 Jan '14

19 Jan '14

Hi, I have asked mathoverflow for formalizations of category theory in proof assistants at http://mathoverflow.net/questions/152497/formalizations-of-category-theory-…, and was told that my list (copied below) was approximately complete. I would like to know if anyone on this list knows of formalizations that I missed; feel free to respond either by email or on the mathoverflow thread. Thanks, Jason The mathoverflow question: The ones I know about are: * https://bitbucket.org/JasonGross/catdb, which became https://github.com/JasonGross/HoTT-categories, which became https://github.com/HoTT/HoTT/tree/master/theories/categories * https://github.com/benediktahrens/Foundations/tree/typesystems * https://github.com/pcapriotti/agda-categories/ * https://github.com/jmchapman/restriction-categories * https://github.com/konn/category-agda * http://coq.inria.fr/pylons/pylons/contribs/view/MathClasses/v8.4 * http://www.cs.berkeley.edu/~megacz/coq-categories/ * http://coq.inria.fr/pylons/pylons/contribs/view/Coalgebras/v8.4 * http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4 * https://github.com/copumpkin/categories * https://github.com/crypto-agda/crypto-agda/tree/master/FunUniverse * http://coq.inria.fr/pylons/pylons/contribs/view/ConCaT/v8.4 * http://coq.inria.fr/pylons/pylons/contribs/view/CatsInZFC/v8.4 * http://mattam.org/repos/coq/cat/ * https://github.com/benediktahrens/rezk_completion * https://github.com/rs-/Triangles * https://github.com/benediktahrens/coinductives I also know about the following papers about formalizing category theory in proof assistants: * "Veriﬁed Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory" by Arnaud Spiwack (http://assert-false.net/arnaud/papers/thesis.spiwack.pdf) * "Galois: a theory development project" by Peter Aczel (http://www.cs.man.ac.uk/~petera/galois.ps.gz) * "A mechanically assisted constructive proof in category theory" by James Altucher and Prakash Panangaden (http://link.springer.com/chapter/10.1007/3-540-52885-7_110) * "Category Theory in Coq" by Carvalho (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9846) * "Category Theory as an Extension of Martin-Lof Type Theory" by http://rd.host.cs.st-andrews.ac.uk/publications/CTMLTT.pdf * "Automating Proofs in Category Theory" by Dexter Kozen, Christoph Kreitz, and Eva Richter (http://www.cs.uni-potsdam.de/ti/kreitz/PDF/06ijcar-categories.pdf) * "Towards a readable formalisation of category theory" by Greg O'Keefe (http://users.cecs.anu.edu.au/~okeefe/work/fcat4cats04.pdf) I'm primarily interested in public-domain code implementing category theory in a proof assistant, though I'm also interested in papers about formalizations of category theory in proof assistants. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0