Adam Chlipala | 2 Apr 16:34 2012
Picon
Picon

Call for papers (deadline change): LFMTP'12 (colocated with ICFP'12)

Apologies for the re-announcement; we've decided to shift the schedule 
later a bit, as reflected below.

=============================================================

Seventh International Workshop on Logical Frameworks
       and Meta-Languages: Theory and Practice
                    (LFMTP'12)

      http://people.csail.mit.edu/adamc/lfmtp12/

Copenhagen, Denmark, September 9, 2012
Affiliated with the
  International Conference on Functional Programming
      (ICFP'12)

   CALL FOR PAPERS

-------------------------------------------------------------
   IMPORTANT DATES

Paper submission:        May 14, 2012
Author notification:     June 18, 2012
Final versions due:      July 2, 2012
Workshop day:            September 9, 2012
-------------------------------------------------------------

Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
(Continue reading)

Peter Höfner | 7 Apr 15:32 2012
Picon

Call for Papera - Automated Theory Exploration (ATx)

                [Apologies if you receive multiple copies of this announcement]
                            *** Deadline extended to 17th April 2012 ***
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                                CALL FOR PAPERS:

                                    ATX-2012
                  IJCAR Workshop on Automated Theory Exploration
                                (June 30-July 1)
                   http://dream.inf.ed.ac.uk/events/atx2012

GENERAL INFORMATION

This Workshop on Automated Theory Exploration will be held in June/July in Manchester, UK.
It is associated with the 6th International Conference on Automated Reasoning (IJCAR) and
follows on from two series of workshops: Automated Theory Engineering and Automatheo.

SCOPE

Theory exploration means the development of mathematical axioms, definitions, conjectures,
theorems, examples and inference procedures as needed to cover the essential concepts
and analysis tasks of mathematical and other application domains. The automation and
mechanisation of these capabilities are much sought after in areas such as software
verification, the analysis of computer systems, formalised mathematics and indeed
mathematical research.

The aim of the workshop is to bring together researchers with interests in any aspects
of this area, including domain-specific formalisations, tool and theory development,
and general-purpose frameworks for the structuring of theories and their maintenance.

TOPICS
(Continue reading)

Takashi KITAMURA | 9 Apr 13:35 2012
Picon

*Deadline Extended* CFP : ICFEM 2012 - 14th International Conference on Formal Engineering Methods

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The deadlines of abstract submissions and paper submissions to ICFEM 2012
have been extended as follows.

Abstract Submission Deadline (Extended):      16th  April, 2012
Full Paper Submission Deadline (Extended):    23th April, 2012

We are looking forward to your submissions.

************************************************************
ICFEM 2012:
14th International Conference on Formal Engineering Methods
CALL FOR PAPERs
12th-16th, November, 2012
Kyoto Research Park, Kyoto, Japan
************************************************************ 

ICFEM will come back to Japan in 2012 again! Since 1997, ICFEM has 
been serving as an international forum for researchers and practitioners
 who have been seriously applying formal methods to practical applications.
Researchers and practitioners, from industry, academia, and government, 
are encouraged to attend, and to help advance the state of
the art. We are interested in work that has been incorporated into
(Continue reading)

Joyal, André | 10 Apr 01:46 2012
Picon

news on the boycott

From Tom Leinster at the n-café:

http://www.guardian.co.uk/science/2012/apr/09/wellcome-trust-academic-spring

http://www.guardian.co.uk/science/2012/apr/09/frustrated-blogpost-boycott-scientific-journals

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Michael Barr | 11 Apr 15:59 2012
Picon

Oktoberfest

We have been thinking of having an Oktoberfest.  Thanksgiving/Columbus
Day is Oct. 8, which has not been the most successful time to have it.  So
either Oct. 13-14 or 20-21 would be good.  Please email me if you are
interested in it and tell me which weekend you prefer.

Michael

--

-- 
An ostrich is more intelligent than the average congressman.  The
ostrich does not bury its head in the sand.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Michael Barr | 12 Apr 16:19 2012
Picon

Dates for Oktoberfest

I have received two irreducible conflicts for Oct. 20-21 and one for the
earlier date (from Robert Dawson) which I copy here:
        I, along with a number of other Atlantic Canadians, will be in
Sackville, NB on the 12-13-14 for the
Science Atlantic (was APICS) math/stats meeting. Thus, the weekend after
would be a better choice for us.

I have to ask how many Atlantic Canadians this will impact?  Also how
about Oct. 27-28 or Sept. 29-30?  How many feel Thanksgiving weekend
creates a problem?

Michael

--

-- 
An ostrich is more intelligent than the average congressman.  The
ostrich does not bury its head in the sand.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Michael Barr | 13 Apr 12:59 2012
Picon

Date for Oktoberfest

It appears that the date with the least number of conflicts is the last
weekend in October.  So be it.  Don't blame me if the weather has turned
nasty by then.

I should have mentioned that it will be at Concordia like the one a few
years ago (thanks, Bob).  McGill has gone out of its way to discourage
(and charge an exhorbitant fee for) this kind of meeting (thanks,
Heather--it's what happens when you get an administrator as principal).

Michael

--

-- 
An ostrich is more intelligent than the average congressman.  The
ostrich does not bury its head in the sand.

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Emily Riehl | 14 Apr 00:09 2012
Picon

orthogonal factorization systems

I've placed a bet with a colleague that the following result appears in
the literature. Please help me win.

Claim: Suppose (E,M) is an orthogonal factorization system (unique lifts)
on a symmetric monoidal category and X is a fixed monoid. If tensoring
with X preserves maps in the class E, then (E,M) lifts to an orthogonal
factorizaiton system on the category of X-modules.

Regards,
Emily Riehl

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Richard Garner | 15 Apr 00:27 2012
Picon
Picon

Re: orthogonal factorization systems

Dear Emily,

You are in luck. Your result is an instance of the following:

PROP
If C is a category bearing the orthogonal factorisation system (E,M),
and T is a monad on C whose underlying functor preserves E-maps, then
C^T bears the orthogonal factorisation system (U^-1(E), U^-1(M)).

A full proof of which is given as Proposition 20.28 in:

Abstract and concrete categories: The joy of cats (Wiley, 1990)
Jiri Adamek, Horst Herrlich and George Strecker

Maybe there is an older reference than this but I am not aware of such.

Richard

On 14 April 2012 08:09, Emily Riehl <eriehl <at> math.harvard.edu> wrote:
> I've placed a bet with a colleague that the following result appears in
> the literature. Please help me win.
>
> Claim: Suppose (E,M) is an orthogonal factorization system (unique lifts)
> on a symmetric monoidal category and X is a fixed monoid. If tensoring
> with X preserves maps in the class E, then (E,M) lifts to an orthogonal
> factorizaiton system on the category of X-modules.
>
> Regards,
> Emily Riehl
>
(Continue reading)

Alessio Guglielmi | 16 Apr 19:38 2012
Picon

University of Bath Prize Fellow

Hello,

I would like to advertise the following positions 
at the University of Bath. In particular we are 
looking for applicants in the area `Software 
verification and correctness´.

Ciao,

-Alessio

Software verification and correctness

We aim to build on the existing strengths within 
the Mathematical Foundations group in the 
Department of Computer Science. The group 
comprises Prof Guy McCusker and Dr Jim Laird 
(semantics), Dr Alessio Guglielmi (proof theory), 
Dr John Power (category theory) and Prof James 
Davenport (computer algebra).

We seek to strengthen its activities via the 
appointment of a Prize Fellow in software 
verification & correctness, to be understood 
broadly, to complement existing expertise; it 
would also be desirable to strengthen connections 
with other groups in the department, particularly 
with Dr Marina De Vos and Dr Julian Padget in the 
Intelligent Systems group. The Fellow would be 
coming into a well-resourced, lively group that 
(Continue reading)


Gmane