Search results for: S. Ronchi Della Rocca

Items from 1 to 7 out of 7 results

chapter

Listing of information structures defined by fixed-point operators

C. Böhm, M. Dezani-Ciancaglini, S. Ronchi Della Rocca

Lecture Notes in Computer Science > Programming Symposium > 266-279

First S-questionnaires are introduced as mechanical devices which permit the representation of recursively definable families of information structures by means of sets of sequences of non-negative integers. The subclass of L-questionnaires is then defined enabling: i) a bijection between such a family F and the set ℕ of non-negative integers ii) the construction of an operator admitting exactly the...

chapter

(Semi)-separability of finite sets of terms in Scott's D_∞-models of the λ-calculus

M. Coppo, M. Dezani-Ciancaglini, S. Ronchi della Rocca

Lecture Notes in Computer Science > Automata, Languages and Programming > 142-164

A finite set {F₁, ...,F_n} of terms of λ-calculus is said to be: separable iff, given n arbitrary terms X₁, ..., X_n, there exists a context C [ ] such that C[F_i]=X_i for 1≤i≤n semi-separable iff, given n−1 arbitrary terms X₁, ..., X_n−1 there exists a context C [ ] such that C [F_i]=X_i for 1≤i ≤n−1 and C [F_n] is unsolvable. In the present paper the constructive characterization...

chapter

Discriminability of infinite sets of terms in the D_∞-models of the λ-calculus

S. Ronchi della Rocca

Lecture Notes in Computer Science > CAAP '81 > 350-364

article

Intersection Types from a Proof-theoretic Perspective

E. Pimentel, S. Ronchi della Rocca, L. Roversi

Fundamenta Informaticae > 2012 > Vol. 121, nr 1/4 > 253-274

In this work we present a proof-theoretical justification for the intersection type assignment system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction,...

article

Linearity, Non-determinism and Solvability

M. Pagani, S. Ronchi della Rocca

Fundamenta Informaticae > 2010 > Vol. 103, nr 1-4 > 173-202

We study the notion of solvability in the resource calculus, an extension of the γ-calculus modelling resource consumption. Since this calculus is non-deterministic, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). We give a syntactical, operational and logical characterization for the may-solvability and only a partial characterization...

article

Principal Typing for Lambda Calculus in Elementary Affine Logic

P. Coppola, S. Ronchi della Rocca

Fundamenta Informaticae > 2005 > Vol. 65, nr 1,2 > 87--112

Elementary Affine Logic (EAL) is a variant of Linear Logic characterizing the computational power of the elementary bounded Turing machines. The EAL Type Inference problem is the problem of automatically assigning to terms of l-calculus EAL formulas as types. This problem, restricted to the propositional fragment of EAL, is proved to be decidable, and an algorithm is shown, building, for every l-term,...

article

Alpha-Conversion and Typability

A.J. Kfoury, S. Ronchi della Rocca, J. Tiuryn, P. Urzyczyn

Information and Computation > 1999 > 150 > 1 > 1-21

There are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-orderλ-calculusFof Girard and Reynolds without affecting the typing power of the system. On the other hand we show that it is impossible to eliminate alpha-conversion on universally quantified variables in the higher-orderλ-calculusF _ω of Girard, by exhibiting a term which is...

Filter options

Publication date

Set your own date range

Content availability

Available (4)
None (3)

Publication type

article (4)
book (3)

Keywords

Data set

BazTech (3)
Springer (3)
Elsevier (1)

Journal

Fundamenta Informaticae (3)
Information and Computation (1)

INFONA - science communication portal

Search results for: S. Ronchi Della Rocca

Listing of information structures defined by fixed-point operators

(Semi)-separability of finite sets of terms in Scott's D∞-models of the λ-calculus

Discriminability of infinite sets of terms in the D∞-models of the λ-calculus

Intersection Types from a Proof-theoretic Perspective

Linearity, Non-determinism and Solvability

Principal Typing for Lambda Calculus in Elementary Affine Logic

Alpha-Conversion and Typability

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Content availability

Publication type

Keywords

Data set

Journal

Reporting an error / abuse

Sending the report failed

Accessibility options

(Semi)-separability of finite sets of terms in Scott's D_∞-models of the λ-calculus

Discriminability of infinite sets of terms in the D_∞-models of the λ-calculus