Sciweavers

LICS
1994
IEEE
13 years 8 months ago
A Multiple-Conclusion Meta-Logic
The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, Prolog and its linear logic ...
Dale Miller
LICS
1996
IEEE
13 years 8 months ago
A Linear Logical Framework
We present the linear type theory LLF as the forThis extended abstract will appear on the proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science -LICS'...
Iliano Cervesato, Frank Pfenning
CADE
1997
Springer
13 years 8 months ago
Connection-Based Proof Construction in Linear Logic
We present a matrix characterization of logical validity in the multiplicative fragment of linear logic. On this basis we develop a matrix-based proof search procedure for this fra...
Christoph Kreitz, Heiko Mantel, Jens Otten, Stepha...
ICLP
1998
Springer
13 years 8 months ago
Efficient Implementation of a Linear Logic Programming Language
A number of logic programming languages based on Linear Logic [3] have been proposed. However, the implementation techniques proposed for these languages have relied heavily on th...
Joshua S. Hodas, K. M. Watkins, Naoyuki Tamura, Ky...
ICLP
1998
Springer
13 years 8 months ago
Compiling Resources in a Linear Logic Programming Language
There have been several proposals for logic programming language based on linear logic: Lolli [6], Lygon [5], LO [3], LinLog [2], Forum [8]. In addition, BinProlog allows the use ...
Mutsunori Banbara, Naoyuki Tamura
TABLEAUX
1999
Springer
13 years 8 months ago
linTAP: A Tableau Prover for Linear Logic
Abstract. linTAP is a tableau prover for the multiplicative and exponential fragment M?LL of Girards linear logic. It proves the validity of a given formula by constructing an anal...
Heiko Mantel, Jens Otten
LICS
1999
IEEE
13 years 8 months ago
Concurrent Games and Full Completeness
A new concurrent form of game semantics is introduced. This overcomes the problems which had arisen with previous, sequential forms of game semantics in modelling Linear Logic. It...
Samson Abramsky, Paul-André Melliès
CSFW
1999
IEEE
13 years 8 months ago
A Meta-Notation for Protocol Analysis
Most formal approaches to security protocol analysis are based on a set of assumptions commonly referred to as the "Dolev-Yao model." In this paper, we use a multiset re...
Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln...
BIRTHDAY
2000
Springer
13 years 9 months ago
Bistructures, bidomains, and linear logic
Bistructures are a generalisation of event structures which allow a representation of spaces of functions at higher types in an orderextensional setting. The partial order of caus...
Pierre-Louis Curien, Gordon D. Plotkin, Glynn Wins...
CSL
2001
Springer
13 years 9 months ago
Non-commutativity and MELL in the Calculus of Structures
We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of m...
Alessio Guglielmi, Lutz Straßburger