The following pages link to (Q3077958):
Displaying 50 items.
- A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization (Q276268) (← links)
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
- De Bruijn's weak diamond property revisited (Q740482) (← links)
- Nominal essential intersection types (Q1643145) (← links)
- Fixed points in lambda calculus. an eccentric survey of problems and solutions (Q1688969) (← links)
- The Cooper storage idiom (Q1711505) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- How to think of intersection types as Cartesian products (Q1744395) (← links)
- Strong normalization through intersection types and memory (Q1744407) (← links)
- Composition and decomposition of multiparty sessions (Q1996856) (← links)
- On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem (Q2062200) (← links)
- Combinatory logic with polymorphic types (Q2144609) (← links)
- Parametric Church's thesis: synthetic computability without choice (Q2151397) (← links)
- Semantics of quantum programming languages: Classical control, quantum control (Q2168785) (← links)
- On some enumerative problems in lambda calculus (Q2202676) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- The untyped computational \(\lambda \)-calculus and its intersection type discipline (Q2210507) (← links)
- A coinductive approach to proof search through typed lambda-calculi (Q2231698) (← links)
- The spirit of node replication (Q2233421) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Typed path polymorphism (Q2424892) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- A Coalgebraic View of Bar Recursion and Bar Induction (Q2811334) (← links)
- Agent-Based HOL Reasoning (Q2819202) (← links)
- A Computable Solution to Partee’s Temperature Puzzle (Q2964003) (← links)
- Metric Reasoning About $$\lambda $$-Terms: The General Case (Q2988646) (← links)
- (Q3300796) (← links)
- (Q3522248) (← links)
- Efficient type checking for path polymorphism (Q4580227) (← links)
- (Q4580329) (← links)
- (Q4625705) (← links)
- COCHIS: Stable and coherent implicits (Q4972074) (← links)
- (Q5013825) (← links)
- Soundness Conditions for Big-Step Semantics (Q5041092) (← links)
- On sets of terms having a given intersection type (Q5043597) (← links)
- Monotone recursive types and recursive data representations in Cedille (Q5076393) (← links)
- A Generic Framework for Higher-Order Generalizations. (Q5089010) (← links)
- (Q5089030) (← links)
- The complexity of principal inhabitation (Q5111311) (← links)
- (Q5119396) (← links)
- The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them (Q5140030) (← links)
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search (Q5236550) (← links)
- Levy Labels and Recursive Types (Q5283442) (← links)
- A characterization of lambda-terms transforming numerals (Q5371970) (← links)
- Clocks for Functional Programs (Q5410452) (← links)
- Almost all Classical Theorems are Intuitionistic (Q5871575) (← links)
- (Q6060673) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- (Q6079229) (← links)
