Journal "Logical Methods in CS"

From the Proof Theory mailing list: the Logical Methods in Computer Science journal (LMCS) has been launched, with the message from the editors:

Dear Colleague:

We are writing to inform you about the progress of the open-access,
online journal "Logical Methods in Computer Science," which has recently
benefited from a freshly designed web site, see:


In the first year of its existence, the journal received 75 submissions:
21 were accepted and 22 declined (the rest are still in the editorial
process). The first issue is complete, and we anticipate
that will be three in all by the end of the calendar year. Our eventual
aim is to publish four issues per year. We also publish Special Issues:
to date, three are in progress, devoted to selected papers from LICS
2004, CAV 2005 and LICS 2005.

The average turn-around from submission to publication has been
7 months. This comprises a thorough refereeing and revision process:
every submission is refereed in the  normal way by two or more
referees, who apply high standards of quality.

We would encourage you to submit your best papers to Logical Methods in
Computer Science, and to encourage your colleagues to do so too.
There is a flier and a leaflet containing basic information about the
new journal on the homepage; we would appreciate your posting
and distributing them, or otherwise publicising the journal. We would
also appreciate any suggestions you may have on how we may improve the

Yours Sincerely,

Dana S. Scott (editor-in-chief)
Gordon D. Plotkin and Moshe Y. Vardi (managing editors)
Jiri Adamek (executive editor)

PS. I would have posted this to the front page, but these privileges have been lost, no doubt for incalcitrant inactivity...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Contributing Editor Status

but these privileges have been lost, no doubt for incalcitrant inactivity...

We don't do that over here. I think the problem is that you have more than one account.

I upgraded the account you used, and promoted the item to the home page.

Deep stuff

Let me just point out that the sort of thing discussed in this journal is pretty deep and abstract, even for theory wonks, so don't be too disappointed or surprised if you don't understand even the titles of the papers...

Depth notwithstanding...

..LtUers might be pleased to see that all LMCS articles are made available under a Creative Commons license: given the already-prestigious nature of this journal, this is likely to have impact on publishing in the discipline. Is it too much to hope the ACM might be shamed into improving its openness policy?


One way to help them make the right decision is to point out that our policy on LtU is to discuss papers that are publicly available online.

A paper has to be truly amazing for me to mention it on the home page if it's only available through the ACM Digital Library.

Yes, CC licensed is great!

I'm a fan of journals with decent content that have a user friendly content license. Shall I advertise The Monad.Reader again?

I also refuse to read pay-only articles. I would be happy to pay the researchers for their time and effort, and for publication, but I do not wish to pay for access. Knuth had something to say about this also.

Ok, I'm off the soapbox now...


When ACM finally open up their digital library to all I predict that LtU will become the most important site on the internet :-)

I predict that LtU will beco

I predict that LtU will become the most important site on the internet

Isn't it already?

Recursion via Coinductive Types - dual to Hyperfunctions?

It seems to me that the General Recursion via Coinductive Types paper is talking about (possibly infinitely) recursive type level computations.

If that's true, does that mean that hyperfunctions are the dual of these sorts of functions?

Alternatively, if this isn't talking about type level computations, does this give a way to do typesafe general recursion in dependently typed languages like Epigram?

Neat paper, the author has more neat papers on his website.

Typesafe general recursion

The answer to your second question isn't the exciting one you might be hoping for. Since any terminating deterministic program can be explicitly assigned a type annotation that tells you in how many steps it terminates, the answer is yes. Since, in the general case, to know what this type annotation is of an arbitrary program before run time is to have a solution to the halting problem, this fact can't be much help.

(fixed sense inverting typos in above)