Zobrazeno 1 - 10
of 13
pro vyhledávání: '"Jeff Polakow"'
Autor:
Jeff Polakow
Publikováno v:
Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.
The original presentation of uniform ordered linear logic does not permit direct implementation (in Olli) as a meta-circular interpreter. We explain the difficulty and present a new formulation of the logic, called uniform atomic ordered linear logic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5be66266e5f18cc69f3630e4a3f15fc3
https://doi.org/10.1145/3130261.3130264
https://doi.org/10.1145/3130261.3130264
Publikováno v:
Haskell
We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary theorem proving by verifying a parallel, monoidal string matching algorithm implemented in Haskell. We use refinement typ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::dff5503cea050f9f0f3759094f9ec0a3
https://doi.org/10.1145/3122955.3122963
https://doi.org/10.1145/3122955.3122963
Autor:
Jeff Polakow
Publikováno v:
Haskell
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 ch
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::557c2c398afa0aefa26ae848855d108c
https://doi.org/10.1145/2804302.2804309
https://doi.org/10.1145/2804302.2804309
Autor:
Jeff Polakow
Publikováno v:
Journal of Logic and Computation. 16:135-155
We present a new system of resource management for linear logic programming which ensures linearity constraints are satisfied solely by manipulating individual formula tags. In our system, tags are rational numbers, and a single bounded interval suff
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aeaa66e069689651a752363fc2499b2a
https://doi.org/10.1093/logcom/exi073
https://doi.org/10.1093/logcom/exi073
Autor:
Joshua S. Hodas, Jeff Polakow
Publikováno v:
Electronic Notes in Theoretical Computer Science. 3:196-207
When Miller introduced Forum he called it a specification logic, rather than a logic programming language. In this paper we outline those features that create problems in attempting to implement an interpreter for the language, and describe solutions
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f484f927fdaa8811e059bb96822beeac
Autor:
Jeff Polakow
Publikováno v:
Proceedings of the 13th ACM SIGPLAN international conference on Functional programming.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9777f8b70878ac89ebd65f1cfe3c3f5e
https://doi.org/10.1145/1411204.2181027
https://doi.org/10.1145/1411204.2181027
Autor:
Jeff Polakow, Christian Skalka
Publikováno v:
PLAS
We propose the monadic linear logic programming language LolliMon as a new foundation for the specification of distributed trust management systems, particularly the RT framework. LolliMon possesses features that make it well-suited to this applicati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::965d9238f913c11a6b6f408ebc74e4bf
https://doi.org/10.1145/1134744.1134753
https://doi.org/10.1145/1134744.1134753
Publikováno v:
PPDP
Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend Lolli with the remaining connectives of intuitionist
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e15bdcda1deebe8b56476c1d94f5def5
https://doi.org/10.1145/1069774.1069778
https://doi.org/10.1145/1069774.1069778
Publikováno v:
Programming Languages and Systems ISBN: 9783540213130
ESOP
ESOP
Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The ! operator, used to distinguish between linear and non-linear types, has good potential for better res
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::88e79c7cd4c0536df4495d7a0222b62e
https://doi.org/10.1007/978-3-540-24725-8_21
https://doi.org/10.1007/978-3-540-24725-8_21
A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines
Autor:
Jeff Polakow, Alberto Momigliano
Publikováno v:
MERLIN
We report on work in progress devoted to the formalization of an Ordered Logical Framework (OLF) [16] based on a two-levels architecture [10] in the Hybrid system [2]. OLF here is a second-order version of ordered linear logic to be used as a meta-la
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9912d5b5e84301345c8ce41d907d8825
https://doi.org/10.1145/976571.976581
https://doi.org/10.1145/976571.976581