Zobrazeno 1 - 10
of 43
pro vyhledávání: '"Jacek Chrząszcz"'
Autor:
Jacek Chrząszcz, Aleksy Schubert
Publikováno v:
Information and Computation. 248:130-149
Soft type assignment systems STA, STA + , and STA B characterise by means of reduction of terms computation in complexity classes PTIME, NP, and PSPACE, respectively. All these systems are inspired by linear logic and include polymorphism similar to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7b33e4de2ce190fdb7c12234869ebf8b
https://doi.org/10.1016/j.ic.2015.12.011
https://doi.org/10.1016/j.ic.2015.12.011
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030035914
VSTTE
VSTTE
This paper presents the first Coq formalisation of the full Java bytecode instruction set and its semantics. The set of instructions is organised in a hierarchy depending on how the instructions deal with the runtime structures of the Java Virtual Ma
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e72191ab2bc7adf02b0a97099187f8a8
https://doi.org/10.1007/978-3-030-03592-1_8
https://doi.org/10.1007/978-3-030-03592-1_8
Autor:
Aleksy Schubert, Jacek Chrząszcz
Publikováno v:
PPDP
Declarative programming features are gradually included in the design of object-oriented languages such as Java and C++. These languages recently adopted anonymous function definitions and offer basic primitives that restrict changes on data, namely
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::93444c84843f21e6a1bd06103690356f
https://doi.org/10.1145/3131851.3131860
https://doi.org/10.1145/3131851.3131860
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783662460771
SOFSEM
SOFSEM
Although there exist rare cases where exponential algorithms are used with success, practical software projects mostly consist of polynomial code. We present an automatic analysis tool which divides while-loops in a Java software project into polynom
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::269654433b99715bd407ddc37dd3b131
https://doi.org/10.1007/978-3-662-46078-8_50
https://doi.org/10.1007/978-3-662-46078-8_50
Publikováno v:
CompSysTech
Contemporary programs come with complex user interfaces hard to analyze without automated support. There are many applications when precise analysis of a system GUI organization is needed and required --- e.g. generation of GUI map. Unfortunately it
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::97adbad7309de994c14b38a8cdfcae1d
https://doi.org/10.1145/2023607.2023621
https://doi.org/10.1145/2023607.2023621
Publikováno v:
Interactive Theorem Proving ISBN: 9783642140518
ITP
ITP
Extending the calculus of constructions with rewriting would greatly improve the efficiency of proof assistants such as Coq. In this paper we address the issue of the logical power of such an extension. In our previous work we proposed a procedure to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aeb613319418b268f339fcbc5e672016
https://doi.org/10.1007/978-3-642-14052-5_31
https://doi.org/10.1007/978-3-642-14052-5_31
Publikováno v:
Automated Reasoning ISBN: 9783540371878
IJCAR
IJCAR
Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable and incons
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ea43711b045838d21e22be89cd0778f
https://doi.org/10.2168/lmcs-4(3:8)2008
https://doi.org/10.2168/lmcs-4(3:8)2008
Publikováno v:
Rewriting, Computation and Proof ISBN: 9783540731467
Rewriting, Computation and Proof
Rewriting, Computation and Proof
Equational reasoning in Coq is not straightforward. For a few years now there has been an ongoing research process towards adding rewriting to Coq. However, there are many research problems on this way. In this paper we give a coherent view of rewrit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::95d6cc5c58059d384ce08e944522b81d
https://doi.org/10.1007/978-3-540-73147-4_6
https://doi.org/10.1007/978-3-540-73147-4_6
Autor:
Jacek Chrząszcz, Jean-Pierre Jouannaud
Publikováno v:
Algebra, Meaning, and Computation ISBN: 9783540354628
Essays Dedicated to Joseph A. Goguen
Essays Dedicated to Joseph A. Goguen
Rigorous program development is notoriously difficult because it involves many aspects, among which specification, programming, verification, code reuse, maintenance, and version management. Besides, these various tasks are interdependent, requiring
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4a1404b318103fc8515b1e220231793e
https://doi.org/10.1007/11780274_12
https://doi.org/10.1007/11780274_12
Publikováno v:
Software Engineering Techniques: Design for Quality ISBN: 9780387393872
SET
SET
Maintaining discipline of code in an evolving software project is known to be difficult. We present Minik, an automatic tool written in Java and for Java, that assists technical managers to enforce high and medium level design decisions on programmer
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::35615e5b7c49e1207081f40246cef9a7
https://doi.org/10.1007/978-0-387-39388-9_34
https://doi.org/10.1007/978-0-387-39388-9_34