The following pages link to (Q3997016):
Displaying 50 items.
- Monoidal computer. I: Basic computability by string diagrams (Q385721) (← links)
- The Scott model of linear logic is the extensional collapse of its relational model (Q418011) (← links)
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus (Q428894) (← links)
- The vectorial \(\lambda\)-calculus (Q529049) (← links)
- Strong normalization from an unusual point of view (Q534700) (← links)
- Cut-elimination in the strict intersection type assignment system is strongly normalizing (Q558418) (← links)
- Filter models for conjunctive-disjunctive \(\lambda\)-calculi (Q672044) (← links)
- Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves (Q673628) (← links)
- Lambda abstraction algebras: representation theorems (Q674002) (← links)
- A completeness result for the simply typed \(\lambda \mu \)-calculus (Q732057) (← links)
- A completeness result for a realisability semantics for an intersection type system (Q882122) (← links)
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation) (Q923069) (← links)
- On strong normalization and type inference in the intersection type discipline (Q930868) (← links)
- Parameter-free polymorphic types (Q958481) (← links)
- Strong normalization property for second order linear logic (Q1044837) (← links)
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732) (← links)
- An algebraic view of the Böhm-out technique (Q1275631) (← links)
- A finite equational axiomatization of the functional algebras for the lambda calculus (Q1283777) (← links)
- Typing untyped \(\lambda\)-terms, or reducibility strikes again! (Q1295368) (← links)
- Set-theoretical and other elementary models of the \(\lambda\)-calculus (Q1314361) (← links)
- An equivalence between lambda- terms (Q1322165) (← links)
- Synthesis of ML programs in the system Coq (Q1322847) (← links)
- Classical logic, storage operators and second-order lambda-calculus (Q1326769) (← links)
- Head linear reduction and pure proof net extraction (Q1342250) (← links)
- The Inf function in the system \(F\) (Q1346636) (← links)
- A conjecture on numeral systems (Q1381438) (← links)
- A fuzzy language. (Q1426245) (← links)
- Behavioural inverse limit \(\lambda\)-models (Q1434350) (← links)
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models (Q1583485) (← links)
- On the algebraic models of lambda calculus (Q1583488) (← links)
- Strong storage operators and data types (Q1805408) (← links)
- Building continuous webbed models for system F (Q1826624) (← links)
- Normalization without reducibility (Q1840460) (← links)
- Pattern matching as cut elimination (Q1882898) (← links)
- Intersection types for explicit substitutions (Q1887145) (← links)
- Strong normalization and typability with intersection types (Q1924327) (← links)
- On phase semantics and denotational semantics in multiplicative-additive linear logic (Q1971797) (← links)
- On the concurrent computational content of intermediate logics (Q1989344) (← links)
- The differential \(\lambda \mu\)-calculus (Q2373711) (← links)
- Intersection-types à la Church (Q2381503) (← links)
- Logical equivalence for subtyping object and recursive types (Q2481559) (← links)
- Compositional characterisations of \(\lambda\)-terms using intersection types (Q2566033) (← links)
- λμ-calculus and Böhm's theorem (Q2732290) (← links)
- Les types de données syntaxiques du système ${\cal F}$ (Q2773019) (← links)
- Les<i>I</i>-types du système ${\cal F}$ (Q2773020) (← links)
- Dedekind completion as a method for constructing new Scott domains (Q2841264) (← links)
- Strongly Normalising Cut-Elimination with Strict Intersection Types (Q2842832) (← links)
- Reducibility (Q2842839) (← links)
- (Q3077958) (← links)
- Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique (Q3128482) (← links)