Embedding a full linear Lambda calculus in Haskell

Autor:	Jeff Polakow
Rok vydání:	2015
Předmět:	Higher-order abstract syntax Domain-specific language Hindley–Milner type system Computer science computer.software_genre Dependent type Curry–Howard correspondence Lambda cube Deductive lambda calculus computer.programming_language Simply typed lambda calculus Natural deduction Programming language System F Type inference Binary lambda calculus Fixed-point combinator Pure type system Type checking TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Church encoding Computer Science::Programming Languages Haskell Functional dependency Generalized algebraic data type Lambda calculus computer Typed lambda calculus Lambda lifting
Zdroj:	Haskell
DOI:	10.1145/2804302.2804309
Popis:	We present an encoding of full linear lambda calculus in Haskell using higher order abstract syntax. By making use of promoted data kinds, multi-parameter type classes and functional dependencies, the encoding allows Haskell to do both linear type checking and linear type inference.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::557c2c398afa0aefa26ae848855d108c https://doi.org/10.1145/2804302.2804309 Zobrazit plný text záznamu