Zobrazeno 1 - 10
of 70
pro vyhledávání: '"A. Polonowski"'
Autor:
Polonowski, Emmanuel
DBGen is a tool for Coq developers. It takes as input the definition of a term structure with bindings annotations and generates definitions and properties for lifting and substitution in the De Bruijn setting, up to the substitution lemma. It provid
Externí odkaz:
http://arxiv.org/abs/1212.0253
Autor:
Crolard, Tristan, Polonowski, Emmanuel
We derive a Hoare-Floyd logic for non-local jumps and mutable higher-order procedural variables from a formul{\ae}-as-types notion of control for classical logic. The main contribution of this work is the design of an imperative dependent type system
Externí odkaz:
http://arxiv.org/abs/1112.2950
Autor:
Crolard, Tristan, Polonowski, Emmanuel
Relying on the formulae-as-types paradigm for classical logic, we define a program logic for an imperative language with higher-order procedural variables and non-local jumps. Then, we show how to derive a sound program logic for this programming lan
Externí odkaz:
http://arxiv.org/abs/1112.1554
Autor:
Polonowski, Emmanuel
We introduce a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environme
Externí odkaz:
http://arxiv.org/abs/1112.1316
Autor:
Polonowski, Emmanuel
This document describes the implementation in SML of the LoopW language, an imperative language with higher-order procedural variables and non-local jumps equiped with a program logic. It includes the user manual along with some implementation notes
Externí odkaz:
http://arxiv.org/abs/0912.5515
Autor:
Crolard, Tristan, Polonowski, Emmanuel
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have been tested using Isabelle/HOL program extraction facility for inductiv
Externí odkaz:
http://arxiv.org/abs/0910.1020
Autor:
Polonowski, Emmanuel
Publikováno v:
TR-LACL (2006) 1-50
In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easily proved, only one of them is usually established (and sometimes none)
Externí odkaz:
http://arxiv.org/abs/0909.5045
Publikováno v:
SAE International Journal of Fuels and Lubricants, 2017 Nov 01. 10(3), 664-671.
Externí odkaz:
https://www.jstor.org/stable/26390369
Autor:
Dumitrescu, Cosmin Emil, Polonowski, Christopher, Fisher, Brian T., Cheng, A. S. (Ed), Lilik, Gregory K., Mueller, Charles J.
Publikováno v:
SAE International Journal of Fuels and Lubricants, 2014 Apr 01. 7(1), 65-81.
Externí odkaz:
https://www.jstor.org/stable/26273060
Autor:
Polonowski, Christopher J., Mueller, Charles J., Gehrke, Christopher R., Bazyn, Tim, Martin, Glen C., Lillo, Peter M.
Publikováno v:
SAE International Journal of Fuels and Lubricants, 2012 Jan 01. 5(1), 51-77.
Externí odkaz:
https://www.jstor.org/stable/26272863