ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 10 Issue 4, August 2009

Guest editorial: Special issue on implicit computational complexity
Patrick Baillot, Jean-Yves Marion, Simona Ronchi Della Rocca
Article No.: 23
DOI: 10.1145/1555746.1555747

A new function algebra of EXPTIME functions by safe nested recursion
Toshiyasu Arai, Naohi Eguchi
Article No.: 24
DOI: 10.1145/1555746.1555748

Bellantoni and Cook have given a function-algebra characterization of the polynomial-time computable functions via an unbounded recursion scheme which is called safe recursion. Inspired by their work, we characterize the exponential-time...

Context semantics, linear logic, and computational complexity
Ugo Dal Lago
Article No.: 25
DOI: 10.1145/1555746.1555749

We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity:...

Extending the loop language with higher-order procedural variables
Tristan Crolard, Emmanuel Polonowski, Pierre Valarcher
Article No.: 26
DOI: 10.1145/1555746.1555750

We extend Meyer and Ritchie's Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loopω) is a natural imperative counterpart of Gödel System T. The...

Sup-interpretations, a semantic method for static analysis of program resources
Jean-Yves Marion, Romain Péchoux
Article No.: 27
DOI: 10.1145/1555746.1555751

The sup-interpretation method is proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. It has been introduced in order to increase the intensionality, that is the number of...

A flow calculus of mwp-bounds for complexity analysis
Neil D. Jones, Lars Kristiansen
Article No.: 28
DOI: 10.1145/1555746.1555752

We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introduce mwp-matrices and define a semantic relation ⊧ C : M, where...

Resource control graphs
Jean-Yves Moyen
Article No.: 29
DOI: 10.1145/1555746.1555753

Resource Control Graphs are an abstract representation of programs. Each state of the program is abstracted by its size, and each instruction is abstracted by the effects it has on the state size whenever it is executed. The abstractions of...