The following pages link to (Q4068054):
Displaying 50 items.
- Typing and computational properties of lambda expressions (Q1819575) (← links)
- On the logic of unification (Q1823935) (← links)
- Domain theoretic models of polymorphism (Q1824612) (← links)
- Building continuous webbed models for system F (Q1826624) (← links)
- Encoding types in ML-like languages (Q1826630) (← links)
- The completeness theorem for typing lambda-terms (Q1839242) (← links)
- Alpha-conversion and typability (Q1854262) (← links)
- Basic theory of \(F\)-bounded quantification. (Q1854309) (← links)
- Relational interpretations of recursive types in an operational setting. (Q1854316) (← links)
- Type-directed specialization of polymorphism. (Q1854317) (← links)
- A sequent calculus for subtyping polymorphic types (Q1854408) (← links)
- On completeness and cocompleteness in and around small categories (Q1896485) (← links)
- A curry-style semantics of interaction: from untyped to second-order lazy \(\lambda\mu\)-calculus (Q2200839) (← links)
- Do judge a test by its cover. Combining combinatorial and property-based testing (Q2233461) (← links)
- Graded modal dependent type theory (Q2233475) (← links)
- Term-generic logic (Q2339466) (← links)
- Domain-theoretical models of parametric polymorphism (Q2464940) (← links)
- Selective strictness and parametricity in structural operational semantics, inequationally (Q2464947) (← links)
- Ensuring termination by typability (Q2500473) (← links)
- A relational account of call-by-value sequentiality (Q2506495) (← links)
- Inductive types and type constraints in the second-order lambda calculus (Q2639842) (← links)
- Syntactic logical relations for polymorphic and recursive types (Q2864153) (← links)
- Proof Assistants for Natural Language Semantics (Q2963996) (← links)
- CPO-models for second order lambda calculus with recursive types and subtyping (Q3142273) (← links)
- A Type Theory for Probabilistic $$\lambda $$–calculus (Q3297838) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- Two extensions of system F with (co)iteration and primitive (co)recursion principles (Q3653093) (← links)
- (Q4175259) (← links)
- An analysis of the Core-ML language: Expressive power and type reconstruction (Q4632418) (← links)
- POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE (Q4637941) (← links)
- Third-order matching in the polymorphic lambda calculus (Q4645813) (← links)
- Monotone (co)inductive types and positive fixed-point types (Q4943545) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Inferring program specifications in polynomial-time (Q5030195) (← links)
- Applications of type theory (Q5044747) (← links)
- Types as parameters (Q5044771) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract) (Q5055747) (← links)
- Martin Hofmann's Case for Non-Strictly Positive Data Types (Q5091141) (← links)
- Type inference in polymorphic type discipline (Q5096210) (← links)
- An extension of system F with subtyping (Q5096247) (← links)
- (Q5101355) (← links)
- Relating system F and \(\lambda 2\): a case study in Coq, Abella and Beluga (Q5111317) (← links)
- (Q5119393) (← links)
- Explicit effect subtyping (Q5120231) (← links)
- (Q5155670) (← links)
- Correctness of compiling polymorphism to dynamic typing (Q5371998) (← links)
- No value restriction is needed for algebraic effects and handlers (Q5372003) (← links)
- Typed equivalence, type assignment, and type containment (Q5881295) (← links)
- A modular construction of type theories (Q5883738) (← links)
