3 Search Results for "Kumar, Ashish"


Document
Translating Proofs from an Impredicative Type System to a Predicative One

Authors: Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)


Abstract
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.

Cite as

Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19,
  author =	{Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar},
  title =	{{Translating Proofs from an Impredicative Type System to a Predicative One}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19},
  URN =		{urn:nbn:de:0030-drops-174801},
  doi =		{10.4230/LIPIcs.CSL.2023.19},
  annote =	{Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti}
}
Document
Planar Maximum Matching: Towards a Parallel Algorithm

Authors: Samir Datta, Raghav Kulkarni, Ashish Kumar, and Anish Mukherjee

Published in: LIPIcs, Volume 123, 29th International Symposium on Algorithms and Computation (ISAAC 2018)


Abstract
Perfect matchings in planar graphs have been extensively studied and understood in the context of parallel complexity [P W Kastelyn, 1967; Vijay Vazirani, 1988; Meena Mahajan and Kasturi R. Varadarajan, 2000; Datta et al., 2010; Nima Anari and Vijay V. Vazirani, 2017]. However, corresponding results for maximum matchings have been elusive. We partly bridge this gap by proving: 1) An SPL upper bound for planar bipartite maximum matching search. 2) Planar maximum matching search reduces to planar maximum matching decision. 3) Planar maximum matching count reduces to planar bipartite maximum matching count and planar maximum matching decision. The first bound improves on the known [Thanh Minh Hoang, 2010] bound of L^{C_=L} and is adaptable to any special bipartite graph class with non-zero circulation such as bounded genus graphs, K_{3,3}-free graphs and K_5-free graphs. Our bounds and reductions non-trivially combine techniques like the Gallai-Edmonds decomposition [L. Lovász and M.D. Plummer, 1986], deterministic isolation [Datta et al., 2010; Samir Datta et al., 2012; Rahul Arora et al., 2016], and the recent breakthroughs in the parallel search for planar perfect matchings [Nima Anari and Vijay V. Vazirani, 2017; Piotr Sankowski, 2018].

Cite as

Samir Datta, Raghav Kulkarni, Ashish Kumar, and Anish Mukherjee. Planar Maximum Matching: Towards a Parallel Algorithm. In 29th International Symposium on Algorithms and Computation (ISAAC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 123, pp. 21:1-21:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.ISAAC.2018.21,
  author =	{Datta, Samir and Kulkarni, Raghav and Kumar, Ashish and Mukherjee, Anish},
  title =	{{Planar Maximum Matching: Towards a Parallel Algorithm}},
  booktitle =	{29th International Symposium on Algorithms and Computation (ISAAC 2018)},
  pages =	{21:1--21:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Hsu, Wen-Lian and Lee, Der-Tsai and Liao, Chung-Shou},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.21},
  URN =		{urn:nbn:de:0030-drops-99695},
  doi =		{10.4230/LIPIcs.ISAAC.2018.21},
  annote =	{Keywords: maximum matching, planar graphs, parallel complexity, reductions}
}
Document
Deductive Verification of Continuous Dynamical Systems

Authors: Ankur Taly and Ashish Tiwari

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)


Abstract
We define the notion of inductive invariants for continuous dynamical systems and use it to present inference rules for safety verification of polynomial continuous dynamical systems. We present two different sound and complete inference rules, but neither of these rules can be effectively applied. We then present several simpler and practical inference rules that are sound and relatively complete for different classes of inductive invariants. The simpler inference rules can be effectively checked when all involved sets are semi-algebraic.

Cite as

Ankur Taly and Ashish Tiwari. Deductive Verification of Continuous Dynamical Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 383-394, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{taly_et_al:LIPIcs.FSTTCS.2009.2334,
  author =	{Taly, Ankur and Tiwari, Ashish},
  title =	{{Deductive Verification of Continuous Dynamical Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{383--394},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2334},
  URN =		{urn:nbn:de:0030-drops-23342},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2334},
  annote =	{Keywords: Deductive Verification, inductive invariants, continuous and hybrid dynamical systems, Theory of Reals}
}
  • Refine by Author
  • 1 Barnawal, Ashish Kumar
  • 1 Blanqui, Frédéric
  • 1 Datta, Samir
  • 1 Felicissimo, Thiago
  • 1 Kulkarni, Raghav
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Parallel algorithms
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Agda
  • 1 Deductive Verification
  • 1 Dedukti
  • 1 Impredicativity
  • 1 Predicativity
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2009
  • 1 2018
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail