Sciweavers

LICS
1999
IEEE
14 years 2 months ago
Type Inference for Recursive Definitions
We consider type systems that combine universal types, recursive types, and object types. We study type inference in these systems under a rank restriction, following Leivant'...
A. J. Kfoury, Santiago M. Pericás-Geertsen
LICS
1999
IEEE
14 years 2 months ago
The Higher-Order Recursive Path Ordering
This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to terms of a typed ...
Jean-Pierre Jouannaud, Albert Rubio
LICS
1999
IEEE
14 years 2 months ago
Towards a Theory of Bisimulation for Local Names
Pitts and Stark have proposed the -calculus as a language for investigating the interaction of unique name generation and higher-order functions. They developed a sound model base...
Alan Jeffrey, Julian Rathke
LICS
1999
IEEE
14 years 2 months ago
Logics with Aggregate Operators
Lauri Hella, Leonid Libkin, Juha Nurmonen, Limsoon...
LICS
1999
IEEE
14 years 2 months ago
Plausibility Measures and Default Reasoning: An Overview
We introduce a new approach to modeling uncertainty based on plausibility measures. This approach is easily seen to generalize other approaches to modeling uncertainty, such as pr...
Joseph Y. Halpern, Nir Friedman
LICS
1999
IEEE
14 years 2 months ago
Guarded Fixed Point Logic
Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of firstorder logic that were recently introduced by Andr
Erich Grädel, Igor Walukiewicz
LICS
1999
IEEE
14 years 2 months ago
A Superposition Decision Procedure for the Guarded Fragment with Equality
We give a new decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. We argue that this method will be more useful in ...
Harald Ganzinger, Hans de Nivelle
LICS
1999
IEEE
14 years 2 months ago
A New Approach to Abstract Syntax Involving Binders
Murdoch Gabbay, Andrew M. Pitts