MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	101–110 of 143 records found matching your query (RSS):

Search & Display Options

Select All Deselect All

[1–10] << 11 12 13 14 15 >>

List View

Citations

Details

	Records
	Author	Intrigila, Benedetto; Salvo, Ivano; Sorgi, Stefano
	Title	A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser			Type	Journal Article
	Year	2001	Publication	Information and Computation	Abbreviated Journal
	Volume	171	Issue	2	Pages	137-155
	Keywords
	Abstract	Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church-Rosser, CR) and weak confluence (or weak Church-Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the NewmanÃ¢â‚¬â„¢s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties.
	Address
	Corporate Author				Thesis
	Publisher	Academic Press, Inc.	Place of Publication	Duluth, MN, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0890-5401	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Intrigila-Salvo-Sorgi:01			Serial	68
Permanent link to this record



	Author	Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
	Title	Intersection types and λ-definability			Type	Journal Article
	Year	2003	Publication	Mathematical Structures in Computer Science	Abbreviated Journal
	Volume	13	Issue	1	Pages	15-53
	Keywords
	Abstract	This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
	Address
	Corporate Author				Thesis
	Publisher	Cambridge University Press	Place of Publication	New York, NY, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0960-1295	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03			Serial	69
Permanent link to this record



	Author	Bucciarelli, Antonio; Salvo, Ivano
	Title	Totality, Definability and Boolean Circuits			Type	Journal Article
	Year	1998	Publication		Abbreviated Journal
	Volume	1443	Issue		Pages	808-819
	Keywords
	Abstract	In the type frame originating from the flat domain of boolean values, we single out elements which are hereditarily total. We show that these elements can be defined, up to total equivalence, by sequential programs. The elements of an equivalence class of the totality equivalence relation (totality class) can be seen as different algorithms for computing a given set-theoretic boolean function. We show that the bottom element of a totality class, which is sequential, corresponds to the most eager algorithm, and the top to the laziest one. Finally we suggest a link between size of totality classes and a well known measure of complexity of boolean functions, namely their sensitivity.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ bucciarelli-salvo:98			Serial	70
Permanent link to this record



	Author	Bucciarelli, Antonio; de Lorenzis, Silvia; Piperno, Adolfo; Salvo, Ivano
	Title	Some Computational Properties of Intersection Types (Extended Abstract)			Type	Journal Article
	Year	1999	Publication		Abbreviated Journal
	Volume		Issue		Pages	109-118
	Keywords	lambda calculusCurry types, intersection types, lambda-definability, lambda-terms, strong normalization
	Abstract	This paper presents a new method for comparing computation-properties of λ-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and λ-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by β-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry types.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ bucciarelli-delorenzis-piperno-salvo:99			Serial	71
Permanent link to this record



	Author	Bono, V.; Salvo, I.
	Title	A CuCh Interpretation of an Object-Oriented Language			Type	Journal Article
	Year	2001	Publication	Electronic Notes in Theoretical Computer Science	Abbreviated Journal
	Volume	50	Issue	2	Pages	159-177
	Keywords
	Abstract	CuCh machine extends pure lambdaÃ‚â€“calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical object-oriented language.
	Address
	Corporate Author				Thesis
	Publisher	Elsevier	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes	BOTH 2001, BohmÃ¢â‚¬â„¢s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001)			Approved	yes
	Call Number	Sapienza @ mari @ Bono-Salvo:BOTH01			Serial	72
Permanent link to this record



	Author	Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro
	Title	A Type Inference Algorithm for Secure Ambients			Type	Journal Article
	Year	2002	Publication	Electronic Notes in Theoretical Computer Science	Abbreviated Journal
	Volume	62	Issue		Pages	83-101
	Keywords
	Abstract	We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario.
	Address
	Corporate Author				Thesis
	Publisher	Elsevier	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes	TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types			Approved	yes
	Call Number	Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01			Serial	73
Permanent link to this record



	Author	Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano
	Title	Mobility Types for Mobile Processes in Mobile Ambients			Type	Journal Article
	Year	2003	Publication	Electr. Notes Theor. Comput. Sci.	Abbreviated Journal
	Volume	78	Issue		Pages
	Keywords
	Abstract	We present an ambient-like calculus in which the open capability is dropped, and a new form of Ã¢â‚¬Å“lightweightÃ¢â‚¬Â process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the Ã¢â‚¬Å“minimalÃ¢â‚¬Â requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Coppo-Dezani-Giovannetti-Salvo:03			Serial	74
Permanent link to this record



	Author	Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
	Title	A Model Checking Technique for the Verification of Fuzzy Control Systems			Type	Conference Article
	Year	2005	Publication	CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06)	Abbreviated Journal
	Volume		Issue		Pages	536-542
	Keywords
	Abstract	Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, DC, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-2504-0-01	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Immt05			Serial	75
Permanent link to this record



	Author	Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe
	Title	Disk Based Software Verification via Bounded Model Checking			Type	Conference Article
	Year	2007	Publication	APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference	Abbreviated Journal
	Volume		Issue		Pages	358-365
	Keywords
	Abstract	One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, DC, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-3057-5	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Bmtd07			Serial	76
Permanent link to this record



	Author	Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
	Title	Interoperability mapping from XML schemas to ER diagrams			Type	Journal Article
	Year	2006	Publication	Data Knowl. Eng.	Abbreviated Journal
	Volume	59	Issue	1	Pages	166-188
	Keywords
	Abstract	The eXtensible Markup Language (XML) is a de facto standard on the Internet and is now being used to exchange a variety of data structures. This leads to the problem of efficiently storing, querying and retrieving a great amount of data contained in XML documents. Unfortunately, XML data often need to coexist with historical data. At present, the best solution for storing XML into pre-existing data structures is to extract the information from the XML documents and adapt it to the data structuresÃ¢â‚¬â„¢ logical model (e.g., the relational model of a DBMS). In this paper, we introduce a technique called Xere (XML entityÃ‚â€“relationship exchange) to assist the integration of XML data with other data sources. To this aim, we present an algorithm that maps XML schemas into entityÃ‚â€“relationship diagrams, discuss its soundness and completeness and show its implementation in XSLT.
	Address
	Corporate Author				Thesis
	Publisher	Elsevier Science Publishers B. V.	Place of Publication	Amsterdam, The Netherlands, The Netherlands	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0169-023x	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Ddimp06			Serial	77
Permanent link to this record