Zobrazeno 1 - 10
of 13
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:
Jacek Chrząszczewski
Publikováno v:
Ochrona Dziedzictwa Kulturowego, Iss 18 (2023)
The town of Wieliczka was founded around a salt mine, which is now a UNESCO World Heritage Site visited by millions of tourists. Due to its geological structure and mining activities, the area was at risk of sinkholes. The subsidence hazard was elimi
Externí odkaz:
https://doaj.org/article/51c3ff24225940fca06f0721d9b89d06
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