Name
Abstract | ||
|---|---|---|
Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda- calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove that the (untyped) terms of this calculus are reducible in polynomial time. We then extend the type system of Soft logic with recursive types. This allows us to consider non-standard types for representing lists. Using these datatypes we examine the concrete expressiveness of Soft lambda-calculus with the example of the insertion sort algorithm. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-24727-2_4 | LECTURE NOTES IN COMPUTER SCIENCE |
Keywords | Field | DocType |
sorting algorithm,linear logic,polynomial time,lambda calculus,type system | Discrete mathematics,Affine logic,Lambda calculus,Computer science,Minimal logic,P,Type theory,Soft computing,Linear logic,Time complexity | Journal |
Volume | ISSN | Citations |
2987 | 0302-9743 | 28 |
PageRank | References | Authors |
1.17 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Patrick Baillot | 1 | 265 | 18.19 |
| Virgile Mogbil | 2 | 69 | 6.77 |