What people are saying - Write a review
We haven't found any reviews in the usual places.
The Girard Translation Extended with Recursion
Decidability of HigherOrder Subtyping with Intersection Types
35 other sections not shown
Other editions - View all
algebra algorithm antichain argument arity arrows atoms axioms binary binary relation bisimulation boolean bound canonical cartesian closed cartesian closed category clause closed category closed term co-cover coalgebras comonad complete Computer Science congruence consider constant constraint construction contains context Corollary corresponding defined definition denote derivation domain elements equations equivalent example exists expression extension fibration finite set first-order fixpoint formula function symbols functor given graph Hence implies induction integer interpretation intuitionistic intuitionistic logic isomorphism labeled lambda calculus language Lemma linear order literals logic programming method modal logic monadic monoidal morphism natural deduction natural numbers normal form object obtained operational semantics operator pair polynomial predicate symbols problem proof Proposition provable prove pullback quantifier reduction relation resolution game restriction result rewriting satisfies semantics sequent sequent calculus solution solvable specification structure subset substitution subtyping Theorem tree unary variables