Sciweavers

ENTCS
2002
112views more  ENTCS 2002»
13 years 11 months ago
Ambient Calculus and its Logic in the Calculus of Inductive Constructions
The Ambient Calculus has been recently proposed as a model of mobility of agents in a dynamically changing hierarchy of domains. In this paper, we describe the implementation of t...
Ivan Scagnetto, Marino Miculan
ENTCS
2002
72views more  ENTCS 2002»
13 years 11 months ago
The synchronized graphs trace the context-sensitive languages
Morvan and Stirling have proved that the context-sensitive languages are exactly the traces of graphs defined by transducers with labelled final states. We prove that this result ...
Chloe Rispal
ENTCS
2002
129views more  ENTCS 2002»
13 years 11 months ago
Eliminating Proofs from Programs
This paper presents a step in the development of an operational approach to program extraction in type theory. In order to get a program from a lambda term, the logical parts need...
Femke van Raamsdonk, Paula Severi
ENTCS
2002
91views more  ENTCS 2002»
13 years 11 months ago
Memoization-Based Proof Search in LF - an Experimental Evaluation of a Prototype
Elf is a general meta-language for the specification and implementation of logical systems in the style of the logical framework LF. Proof search in this framework is based on the...
Brigitte Pientka
ENTCS
2002
64views more  ENTCS 2002»
13 years 11 months ago
States of Knowledge
Rohit Parikh
ENTCS
2002
91views more  ENTCS 2002»
13 years 11 months ago
Interval Duration Logic: Expressiveness and Decidability
We investigate a variant of dense-time Duration Calculus which permits model checking using timed/hybrid automata. We define a variant of the Duration Calculus, called Interval Du...
Paritosh K. Pandya
ENTCS
2002
152views more  ENTCS 2002»
13 years 11 months ago
Abstract Logics as Dialgebras
Logics as Dialgebras Alessandra Palmigiano Departament de L`ogica, Hist`oria i Filosofia de la Ci`encia, Universitat de Barcelona The aim of this report is to propose a line of re...
Alessandra Palmigiano
ENTCS
2002
76views more  ENTCS 2002»
13 years 11 months ago
Four equivalent equivalences of reductions
Two co-initial reductions in a term rewriting system are said to be equivalent if they perform the same steps, albeit maybe in a different order. We present four characterisations...
Vincent van Oostrom, Roel C. de Vrijer
ENTCS
2002
90views more  ENTCS 2002»
13 years 11 months ago
Inorder traversal of splay trees
Splay trees, a form of self-adjusting binary tree, were introduced by Sleator and Tarjan in the early 1980s. Their main use is to store ordered lists. The idea is to keep the tree...
Colm Ó'Dúnlaing
ENTCS
2002
181views more  ENTCS 2002»
13 years 11 months ago
Alias verification for Fortran code optimization
Abstract: Alias analysis for Fortran is less complicated than for programming languages with pointers but many real Fortran programs violate the standard: a formal parameter or a c...
Thi Viet Nga Nguyen, François Irigoin