@article{MTMT:33527404,
	title = {Tropical Abstraction of Biochemical Reaction Networks with Guarantees},
	url = {https://m2.mtmt.hu/api/publication/33527404},
	author = {Beica, A. and Feret, J. and Petrov, T.},
	doi = {10.1016/j.entcs.2020.06.002},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {350},
	unique-id = {33527404},
	issn = {1571-0661},
	year = {2020},
	pages = {3-32}
}

@article{MTMT:33340064,
	title = {Eilenberg-Kelly Reloaded},
	url = {https://m2.mtmt.hu/api/publication/33340064},
	author = {Uustalu, T. and Veltri, N. and Zeilberger, N.},
	doi = {10.1016/j.entcs.2020.09.012},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {352},
	unique-id = {33340064},
	issn = {1571-0661},
	year = {2020},
	pages = {233-256}
}

@article{MTMT:32638566,
	title = {A Note on Constructive Interpolation for the Multi-Modal Logic K},
	url = {https://m2.mtmt.hu/api/publication/32638566},
	author = {Bárcenas, Everardo and Lavalle-Martínez, José-de-Jesús and Molero-Castillo, Guillermo and Velázquez-Mena, Alejandro},
	doi = {10.1016/j.entcs.2020.10.002},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {354},
	unique-id = {32638566},
	issn = {1571-0661},
	year = {2020},
	pages = {3-16}
}

@article{MTMT:31764468,
	title = {Static Analysis and Stochastic Search for Reachability Problem},
	url = {https://m2.mtmt.hu/api/publication/31764468},
	author = {Chai, Xinwei and Ribeiro, Tony and Magnin, Morgan and Roux, Olivier and Inoue, Katsumi},
	doi = {10.1016/j.entcs.2020.06.008},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {350},
	unique-id = {31764468},
	issn = {1571-0661},
	abstract = {This paper focuses on a major improvement on the analysis of reachability properties in large-scale dynamical biological models. To tackle such models, where classical model checkers fail due to state space explosion led by exhaustive search. Alternative static analysis approaches have been proposed, but they may also fail in certain cases due to non-exhaustive search. In this paper, we introduce a hybrid approach ASPReach, which combines static analysis and stochastic search to break the limits of both approaches. We tackle this issue on a modeling framework we recently introduced, Asynchronous Binary Automata Network (ABAN). We show that ASPReach is able to analyze efficiently some reachability properties which could not be solved by existing methods. We studied also various cases from biological literature, emphasizing the merits of our approach in terms of conclusiveness and performance.},
	keywords = {HEURISTICS; Model checking; Answer set programming; Reachability problem; Asynchronous Binary Automata Network; Local Causality Graph},
	year = {2020},
	pages = {139-158}
}

@article{MTMT:31727720,
	title = {Parametrized Fixed Points and Their Applications to Session Types},
	url = {https://m2.mtmt.hu/api/publication/31727720},
	author = {Kavanagh, Ryan},
	doi = {10.1016/j.entcs.2020.09.008},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {352},
	unique-id = {31727720},
	issn = {1571-0661},
	abstract = {Parametrized fixed points are of particular interest to denotational semantics and are often given by "dagger operations" [10-12]. Dagger operations that satisfy the Conway identities [10] are particularly useful, because these identities imply a large class of identities used in semantic reasoning. We generalize existing techniques to define dagger operations on omega-categories and on O-categories. These operations enjoy a 2-categorical structure that implies the Conway identities. We illustrate these operators by considering applications to the semantics of session-typed languages.},
	keywords = {Fixed points; O-categories; omega-categories; dagger operations; Conway identities},
	year = {2020},
	pages = {149-172}
}

@article{MTMT:32647800,
	title = {A GRASP for the Convex Recoloring Problem in Graphs},
	url = {https://m2.mtmt.hu/api/publication/32647800},
	author = {Dantas, Ana Paula dos Santos and de Souza, Cid Carvalho and Dias, Zanoni},
	doi = {10.1016/j.entcs.2019.08.034},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {346},
	unique-id = {32647800},
	issn = {1571-0661},
	year = {2019},
	pages = {379-391}
}

@article{MTMT:31576782,
	title = {Adapting The Directed Grid Theorem into an FPT Algorithm},
	url = {https://m2.mtmt.hu/api/publication/31576782},
	author = {Campos, Victor and Lopes, Raul and Maia, Ana Karolinna and Sau, Ignasi},
	doi = {10.1016/j.entcs.2019.08.021},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {346},
	unique-id = {31576782},
	issn = {1571-0661},
	abstract = {Originally proved in 1986 by Robertson and Seymour, the Grid Theorem is one of the most important tools in the field of structural graph theory, finding numerous applications in the design of algorithms for undirected graphs. An analogous version of the Grid Theorem isn directed graphs was conjectured by Johnson et al. in 2001, and proved recently by Kawarabayashi and Kreutzer in 2015. Namely they showed that there is a function f (k) such that every directed graph of directed tree-width at least f (k) contains a cylindrical grid of size k as a butterfly minor. Moreover, they claim that their proof can be turned into an XP algorithm, with parameter k, that either constructs a decomposition of the appropriate width, or finds the claimed large cylindrical grid as a butterfly minor. In this article, we adapt some of the steps of the proof of Kawarabayashi and Kreutzer and we improve the XP algorithm into an FPT algorithm.The first step of the proof is an XP algorithm by Johnson et al. in 2001 that decides whether a directed graph D has directed tree-width at most 3k - 2 or admits a haven of order k. It is worth mentioning that a skecth of an FPT algorithm for this problem appears in Chapter 9 of the book "Classes of Directed Graphs", from 2018, with an approximation factor of 5k + 2. Our first contribution is to adapt the proof from Johnson et al. to find either an arboreal decomposition of width at most 3k - 2 or a haven of order k in a directed graph D in FPT time by making use of important separators. We then follow the roadmap of the proof by Kawarabayashi and Kreutzer by locally improving the complexity at some steps, in particular concerning the problem of finding hitting sets for brambles of large order.},
	keywords = {Directed graphs; FPT algorithms; Directed tree-width; grid theorem},
	year = {2019},
	pages = {229-240}
}

@article{MTMT:31202317,
	title = {The Construction of Set-Truncated Higher Inductive Types},
	url = {https://m2.mtmt.hu/api/publication/31202317},
	author = {van der Weide, Niels and Geuvers, Herman},
	doi = {10.1016/j.entcs.2019.09.014},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {347},
	unique-id = {31202317},
	issn = {1571-0661},
	abstract = {We construct finitary set-truncated higher inductive types (HITs) from quotients and the propositional truncation. For that, we first define signatures as a modification of the schema by Basold et al., and we show they give rise to univalent categories of algebras in both sets and setoids. To interpret HITs, we use the well-known method of initial algebra semantics. The desired algebra is obtained by lifting the quotient adjunction to the level of algebras and adapting Dybjer's and Moeneclaey's interpretation of HITs in setoids. From this construction, we conclude that the equality types of HITs are freely generated and that HITs are unique. The results are formalized in the UniMath library.},
	keywords = {Coq; category theory; higher inductive types; homotopy type theory; setoids; intuitionistic type theory},
	year = {2019},
	pages = {261-280}
}

@article{MTMT:31134255,
	title = {On Coloring a Class of Claw-free Graphs},
	url = {https://m2.mtmt.hu/api/publication/31134255},
	author = {Dai, Y. and Foley, A.M. and Hoàng, C.T.},
	doi = {10.1016/j.entcs.2019.08.033},
	editor = {Coutinho, G. and Kohayakawa, Y. and Santos, V.d. and Urrutia, S.},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {346},
	unique-id = {31134255},
	issn = {1571-0661},
	abstract = {Given a set L of graphs, a graph G is L-free if G does not contain any graph in L as an induced subgraph. Recently, Frédéric Maffray and co-authors showed that the problem of coloring {claw, 4K1, K5 \\ e}-free graphs can be solved in polynomial time. In this paper, we investigate a related class of graphs. A hole is an induced cycle of length at least 4. Two vertices x, y of a graph G are twins if for any vertex z different from x and y, xz is an edge if and only if yz is an edge. A hole-twin is the graph obtained from a hole by adding a vertex that forms a twin with some vertex of the hole. Hole-twins, and K5 \\ e, are interesting in their connection with line-graphs. They are among the forbidden subgraphs in the characterization of line-graphs. In this paper, we show there is a polynomial time algorithm to color (claw, 4K1, hole-twin)-free graphs. © 2019 The Author(s).},
	keywords = {Polynomial approximation; Graph theory; Graph coloring; Graphic methods; Line graph; Graph colorings; Claw; Claw; C4-twin; C4-twin; C5-twin; C5-twin; C6-twin; C6-twin; Hole-twin; Hole-twin; Line-Graph; P5-twin; P5-twin},
	year = {2019},
	pages = {369-377}
}

@article{MTMT:31134173,
	title = {Graphs with Girth at Least 8 are b-continuous},
	url = {https://m2.mtmt.hu/api/publication/31134173},
	author = {Ibiapina, A. and Silva, A.},
	doi = {10.1016/j.entcs.2019.08.059},
	editor = {Coutinho, G. and Kohayakawa, Y. and Santos, V.d. and Urrutia, S.},
	journal-iso = {ELECTR NOTES COMPUT SCI},
	journal = {ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE},
	volume = {346},
	unique-id = {31134173},
	issn = {1571-0661},
	abstract = {A b-coloring of a graph is a proper coloring such that each color class has at least one vertex which is adjacent to each other color class. The b-spectrum of G is the set Sb(G) of integers k such that G has a b-coloring with k colors and b(G) = maxSb(G) is the b-chromatic number of G. A graph is b-continous if Sb(G)=[χ(G),b(G)]∩. An infinite number of graphs that are not b-continuous is known. It is also known that graphs with girth at least 10 are b-continuous. In this work, we prove that graphs with girth at least 8 are b-continuous, and that the b-spectrum of a graph G with girth at least 7 contains the integers between 2χ(G) and b(G). This generalizes a previous result by Linhares-Sales and Silva (2017), and tells that graphs with girth at least 7 are, in a way, almost b-continuous. © 2019 The Author(s).},
	keywords = {COLOR; Graph theory; Bipartite graphs; Bipartite graphs; Proper coloring; Graphic methods; Girth; Girth; B-chromatic number; B-chromatic number; b-continuity; Infinite numbers; Spectrum of a graph},
	year = {2019},
	pages = {677-684}
}