The following pages link to (Q4722037):
Displaying 45 items.
- A Glimpse of $$ \sum_{3} $$-elementarity (Q5013913) (← links)
- (Q5020646) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Open problems in rewriting (Q5055780) (← links)
- A termination ordering for higher order rewrite systems (Q5055816) (← links)
- Higher-order narrowing with definitional trees (Q5055857) (← links)
- Higher-order families (Q5055875) (← links)
- Higher-order order-sorted algebras (Q5096189) (← links)
- Wrapper semantics of an object-oriented programming language with state (Q5096238) (← links)
- Principal type-schemes of BCI-lambda-terms (Q5096242) (← links)
- Higher order disunification: Some decidable cases (Q5096304) (← links)
- Higher order conditional rewriting and narrowing (Q5096313) (← links)
- Higher-order narrowing with convergent systems (Q5096386) (← links)
- (Q5101343) (← links)
- Abstract machines, optimal reduction, and streams (Q5108536) (← links)
- Logic and Geometry of Agents in Agent-Based Modeling (Q5150306) (← links)
- A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains (Q5179011) (← links)
- Introduction to Type Theory (Q5191087) (← links)
- Decidable higher-order unification problems (Q5210802) (← links)
- On Some Semi-constructive Theories Related to Kripke–Platek Set Theory (Q5214791) (← links)
- Natural Deduction for Equality: The Missing Entity (Q5251187) (← links)
- RPO, Second-Order Contexts, and λ-Calculus (Q5458369) (← links)
- Types for Hereditary Head Normalizing Terms (Q5458437) (← links)
- (Q5694704) (← links)
- The Church-Rosser property in symmetric combinatory logic (Q5718674) (← links)
- Termination of combined (rewrite and λ-calculus) systems (Q5881181) (← links)
- Extended term rewriting systems (Q5881265) (← links)
- Typed equivalence, type assignment, and type containment (Q5881295) (← links)
- Higher-order unification, polymorphism, and subsorts (Q5881304) (← links)
- An investigation into functions as processes (Q5890045) (← links)
- Type system in programming languages (Q5942703) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
- Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models (Q5958296) (← links)
- Completeness of type assignment systems with intersection, union, and type quantifiers (Q5958301) (← links)
- On the proof theory of Coquand's calculus of constructions (Q5961667) (← links)
- On extensibility of proof checkers (Q6061878) (← links)
- A correct-by-construction conversion from lambda calculus to combinatory logic (Q6065511) (← links)
- The placeholder view of assumptions and the Curry-Howard correspondence (Q6066988) (← links)
- Simultaneous substitution in the typed lambda calculus (Q6116572) (← links)
- Encoding a dependent-type λ-calculus in a logic programming language (Q6488533) (← links)
- Higher order E-unification (Q6488561) (← links)
- System \(F^\mu_\omega\) with context-free session types (Q6535246) (← links)
- A logical aspect of parametric polymorphism (Q6560174) (← links)
- Fundamentals of context-sensitive rewriting (Q6573934) (← links)
- Theoretical computer science: computability, decidability and logic (Q6602262) (← links)
