Jawahar Chirimar, James Lipton
We prove the decidability of the Tensor-Bang fragment of linear logic and establish upper (doubly exponential) and lower (NP-hard) bounds. 1
Realizability, Set Theory and Term Extraction (2007)
James Lipton, In Memoriam, Stephen Kleene
Applicative Structure : : : : : : : : : : : : : : : : : : : : : : : : : : : : 16 3.2 Realizability : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 17 3.3 Soundness for...
Jawahar Chirimar, James Lipton
We prove the decidability of the Tensor-Bang fragment of linear logic and establish upper (doubly exponential) and lower (NP-hard) bounds. 1
Uniform Algebras: A Complete semantics for Higher Order Logic programming with HOHH Formulae. (2007)
This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the lambda-Prolog programming language. Based on an intuitionistic...
Uniform Algebras: A Complete semantics for (2007)
The problem of finding sound and complete semantics for the logic underlying the lambdaProlog programming language: Higher Order Hereditarily Harrop formulas with resolution (uniform) proofs has been...
Eastwood, Clint, Swank, Hilary, Freeman, Morgan, Lipton, James (entrevista)
Presentación en dos DVD del vigésimo quinto largometraje dirigido por el veterano norteamericano Clint Eastwood, quien inició en 1955 su trayectoria como actor de cine y 16 años después...
Hiord: A type-free higher-order logic programming langugae with predicate abstraction (2004)
Daniel Cabeza, Manuel Hermenegildo, James Lipton
Abstract. A new formalism, called Hiord, for defining type-free higherorder logic programming languages with predicate abstraction is introduced. A model theory, based on partial combinatory...
A New Framework For Declarative Programming (2003)
Stacy E. Finkelstein, Peter Freyd, James Lipton, Communicated G. Levi
We propose a new framework for the syntax and semantics of WeakHereditaril Harroplrro programming with constraints, based onresolUf;: over #-categories: #nite product categories with canonical...
Some notes on logic programming with a relational machine (1998)
We study the use of relation calculi for compilation and execution of Horn Clause programs with an extended notion of input and output. We consider various other extensions to the Prolog core. 0
Some Notes on Logic Programming with a Relational Machine (Extended Abstract) (1998)
) James Lipton Emily Chapman Dept. of Mathematics, Wesleyan University Abstract We study the use of relation calculi for compilation and execution of Horn Clause programs with an extended notion of...
Encapsulating data in Logic Programming via Categorical Constraints (1998)
We define a framework for writing executable declarative specifications which incorporate categorical constraints on data, Horn Clauses and datatype specification over finite-product categories. We...
James Lipton, Lauchli Countermodels, Michael J. O'donnell
We use formal semantic analysis based on new, model-theoretic constructions to generate intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive...
Logic Programming in Tau Categories (1995)
Stacy E. Finkelstein, Peter Freyd, James Lipton
Many features of current logic programming languages are not captured by conventional semantics. Their fundamentally non-ground character, and the uniform way in which such languages have been...
Intuitive Counterexamples for Constructive Fallacies (1994)
James Lipton, Michael J. O'donnell
Formal countermodels may be used to justify the unprovability of formulae in the Heyting calculus (the best accepted formal system for constructive reasoning), on the grounds that unprovable formulae...
Intuitive Counterexamples for Constructive Fallacies (1994)
James Lipton, Michael J. O'donnell
Formal countermodels may be used to justify the unprovability of formulae in the Heyting calculus (the best accepted formal system for constructive reasoning), on the grounds that unprovable formulae...
Provability in TBLL: A Decision Procedure (1993)
Chirimar, Jawahar, Lipton, James
We prove the decidability of the Tensor-Bang fragment of linear logic and establish upper (doubly exponential) and lower (NP-hard) bounds.
Some Kripke Models for "one universe" Martin-Lof Type Theory (1990)
We define several Kripke models sound for inhabited formulas of the ground-level intensional and extensional Martin-Lof Type theories with one universe. They are Kripke model versions of the...
Realizability and Kripke Forcing (1990)
Realizability, developed by Stephen Kleene, is a type-free device for extracting computations from logical specifications. Realizability analyzes the computational content of reasoning: it models the...
Some Kripke Models for "one universe" Martin-Lof Type Theory (1990)
We define several Kripke models sound for inhabited formulas of the ground-level intensional and extensional Martin-Lof Type theories with one universe. They are Kripke model versions of the...
Realizability and Kripke Forcing (1990)
Realizability, developed by Stephen Kleene, is a type-free device for extracting computations from logical specifications. Realizability analyzes the computational content of reasoning: it models the...