Research Statement

In the past years, I was fortunate enough to be in contact with many brillant researchers who introduced me to a variety of research topics and influenced (and still have an impact) on my research. I currently have different, but related research interests:

  • Proof Theory and Logical Frameworks
  • Foundations of Computer Security
  • Denotational Semantics of Programming Languages
  • Formal Methods applied to Networking

More details can be found here.

List of Publications/Preprints

Drafts

  • Formal Specification and Verification of a Selective Defense for VoIP DDoS Attacks by Y. Dantas, V.Nigam, I. Fonseca, and P. Cleis. Submitted [pdf].

  • An Executable Formal Model for Specifying and Verifying Clinical Trials by V.Nigam and C. Talcott. Technical Report [pdf].

  • On the Complexity of Verifying Cyber-Physical Security Protocols by M. Kanovich, T. Ban Kirigin, V. Nigam, A. Scedrov and C. Talcott. [pdf].

  • Proof-Relevant Logical Relations for Name Generation by N. Benton, M. Hofmann and V. Nigam. [pdf]. This extends our TLCA’13 paper.

  • On subexponentials, focusing and modalities in concurrent systems by V. Nigam, C. Olarte and E. Pimentel. [pdf]. This extends our CONCUR’13 paper.

  • A Rewriting Framework and Logic for Activities Subject to Regulations by M. Kanovich, T. Ban Kirigin, V. Nigam, A. Scedrov, C. Talcott, and R. Perovic. [pdf]. This extends our RTA’12 paper.

  • Bounded memory Dolev-Yao adversaries in collaborative systems by M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov. Extended version of the FAST 2010 paper. Accepted to Information and Computation. [pdf]

2014

  • A Selective Defense for Application Layer DDoS Attacks by Y. Dantas, V. Nigam and I. Fonseca. Accepted to ISI-EISIC-2014. [pdf]

  • Bounded Memory Protocols by M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov. In Computer Languages, Systems and Structures (COMLAN). [pdf][doi]. This extends our ESORICS’13 paper.

  • An Extended Framework for Specifying and Reasoning about Proof Systems by V. Nigam, E. Pimentel, and G. Reis. Extended version of the LSFA 2010 paper. In the special issue of the J. of Logic and Computation in honor of Roy Dyckhoff. [pdf] [doi] The on-line tool, called TATU, implementing the techniques described in the paper can be found here.

  • A Framework for Linear Authorization Logics by V. Nigam. Theoretical Computer Science (2014), pp. 21-41 [pdf] [doi]. This is an extended and corrected version of my LICS 2012 paper.

  • Quati: An Automated Tool for Proving Permutation Lemmas by V. Nigam, G. Reis, and L. Lima. Accepted to IJCAR. [pdf].

  • A Proof Theoretic Study of Soft Concurrent Constraint Programming by V. Nigam, C. Olarte, and E. Pimentel. Accepted to ICLP. [pdf].

  • Abstract Effects and Proof-Relevant Logical Relations by N. Benton, M. Hofmann and V. Nigam. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 619-631, 2014. [pdf] with some corrections, dated 5 May 2014.

  • Dynamic Spaces in Concurrent Constraint Programming by C. Olarte, V. Nigam and E. Pimentel. Electr. Notes Theor. Comput. Sci. 305, 103-121, 2014 . [pdf]

  • Quati: From Linear Logic Specifications to Inference Rules (Extended Abstract) by V. Nigam, G. Reis, and L. Lima. In Brazilian Meeting of Logic (EBL) Proceedings, 2014 (Informal Proceedings). [pdf]

  • Towards Timed Models for Cyber-Physical Security Protocols by M. Kanovich, T. Ban Kirigin, V. Nigam, A. Scedrov and C. Talcott. In Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography (FCC-FCS), 2014 (Informal Proceedings) [pdf].

  • Towards a Rewriting Framework for Textual Entailment by V. Nigam and V. de Paiva. LSFA, 2014 (Informal Proceedings) [pdf].

2013

  • Relating Focused Proofs with Different Polarity Assignments. by V. Nigam and E. Pimentel. Accepted as Work in Progress in LFMTP 2013. [pdf]

  • Bounded Memory Protocols and Progressing Collaborative Systems by M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov. In J. Crampton, S. Jajodia and K. Mayesthe (Eds): 18th European Symposium on Research in Computer Security (ESORICS) LNCS vol. 8134, pp. 309–326 Springer Verlag, 2013. [pdf]

  • A General Proof System for Modalities in Concurrent Constraint Programming by V. Nigam, C. Olarte, and E. Pimentel. In P.R. D’Argenio and H. Melgratti (Eds.): 24th International Conference on Concurrency Theory (CONCUR 2013), LNCS vol. 8052, pp. 410–424. Springer Verlag, 2013. [pdf] (with Appendix)

  • Checking Proof Transformations with ASP by V. Nigam, G. Reis, and L. Lima. Technical Communication at ICLP 2013. In TPLP, vol. 13, 4-5-Online-Supplement, 2013. [pdf].

  • Proof-Relevant Logical Relations for Name Generation by N. Benton, M. Hofmann, and V. Nigam. In 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013, pages 48-60, LNCS, Springer. [pdf] doi:10.1007/978-3-642-38946-7_6 The technical report of this paper with many more details and extensions can be found here.

2012

  • On the Complexity of Linear Authorization Logics by V. Nigam. In 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pages 511-520, IEEE, 2012. [pdf] (Superseded by A Framework for Linear Authorization Logics)

  • A Rewriting Framework for Activities Subject to Regulations by M. Kanovich, T. Ban Kirigin, V. Nigam, A. Scedrov, C. Talcott, and R. Perovic. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), pages 305-322, LIPIcs v.15, 2012. [pdf]. It is subsumed by the document above: A Rewriting Framework and Logic for Activities Subject to Regulations.

  • Maintaining Distributed Logic Programs Incrementally by V. Nigam, L. Jia, B. T. Loo, A. Scedrov. Extended version of the PPDP 2011 paper. Computer Languages, Systems and Structures (COMLAN) volume 38, pp. 158 – 180, Elsevier Publishing, 2012. [pdf] doi:10.1016/j.cl.2012.02.001

  • FSR: Formal Analysis a Implementation Toolkit for Safe Inter-domain Routing by A. Wang, L. Jia, W. Zhou, Y. Ren, B. T. Loo, J. Rexford, V. Nigam, A. Scedrov, and C. Talcott. IEEE/ACM Transactions on Networking (ToN), volume 20, number 6, pages 1814-1827, 2012. [pdf] doi:10.1109/TNET.2012.2187924

  • Towards an Automated Assistant for Clinical Investigations by V. Nigam, T. Ban Kirigin, A. Scedrov, C. Talcott, M. Kanovich, and R. Perovic. In Second ACM SIGHIT International Health Informatics Symposium (IHI’12), 2012. ACM Digital Libray. [pdf]

2011

  • Maintaining Distributed Logic Programs Incrementally by V. Nigam, L. Jia, B. T. Loo, A. Scedrov. In 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2011), pages 125-136. ACM, 2011. [pdf]. (Superseded by the journal paper above with the same title.) The technical report for this paper can be found here.

  • Specifying proof systems in linear logic with subexponentials by V. Nigam, E. Pimentel, and G. Reis. In LSFA 2010, ENTCS, volume 269, pages 109 – 123, 2011. (Superseded by An Extended Framework for Specifying and Reasoning about Proof Systems.) [pdf]

2010

  • Bounded memory Dolev-Yao adversaries in collaborative systems by M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov. In Formal Aspects of Security and Trust (FAST) 2010 volume 6561 of LNCS, pages 18–33, Springer Verlag, 2010. [pdf].

  • Progressing collaborative systems by M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov. In FCS-PrivMod, a workshop affiliated to both CSF’10 and LICS’10, 2010. [pdf] The implementations described in this paper can be found here.

  • An operational semantics for Network Datalog by V. Nigam, L. Jia, A. Wang, B. T. Loo, and A. Scedrov. In LAM’10, a workshop affiliated to LICS’10, 2010. [pdf] You can also find the extended version of this paper here.

  • A framework for proof systems by V. Nigam and D. Miller. In the special edition of the Journal of Automated Reasoning (JAR) with invited papers from IJCAR 2008, volume 45, issue 2, pages 157-188. 2010 [pdf] doi:10.1007/s10817-010-9182-1

2009

  • Exploiting non-canonicity in the sequent calculus by V. Nigam.. PhD thesis, Ecole Polytechnique, France, 2009. [Thesis homepage].

  • Reach everything from anywhere by J. A. Cordero, U. Herberg and V. Nigam. Obtained the first place in the IPv6Challenge, organized by G6. Report dated 4 June 2009. We also made a short video presentation which can be found here. [pdf]

  • Algorithmic specifications in linear logic with subexponentials by V. Nigam and D. Miller. In Antonio Porto and Francisco Javier Lopez-Fraguas, editors, 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2009), pages 129-140. ACM, 2009 [pdf] The section on subexponential quantifiers is superseded by the CONCUR’13 paper above.

2008

  • Focusing in Linear Meta-Logic by V. Nigam and D. Miller. In A. Armando, P. Baumgartner, G. Dowek, editors, 4th International Joint Conference on Automated Reasoning (IJCAR 2008), volume 5195 of LNCS, pages 507-522. Springer Verlag, 2008 [pdf]. Presentation [pdf]. Subsumed by “A framework for proof systems”.

  • Using Tables to Construct Non-Redundant Proofs by V. Nigam. In A. Beckmann, C. Dimitracopoulos, and B. Loewe editors, CiE 2008: Abstracts and extended abstracts of unpublished papers, 2008 [pdf].

2007

  • Incorporating tables into proofs by D. Miller and V. Nigam. In R. Duparc, T. A. Henzinger, editors, 16th Conference on Computer Science and Logic, (CSL07), volume 4646 of LNCS, pages 466-480. Springer Verlag, 2007 [pdf]. Presentation [pdf]

  • Adding Knowledge Updates to 3APL by V. Nigam and J. Leite. In R. Bordini, M. Dastani, J. Dix, and A. El F. Seghrouchni, editors, 4th International Workshop on Programming Multi-Agent Systems, (ProMAS06), volume 4411 of LNAI, pages 167-183. Springer Verlag, 2007 [pdf].

2006

  • Dynamic Logic Programming and 3APL by V. Nigam. Master thesis, Technische Universität Dresden and Universidade Nova Lisboa, 2006 [pdf].

  • A Dynamic Logic Programming Based System for Agents with Declarative Goals by V. Nigam and J. Leite. In M. Baldoni and U. Endriss, editors, Declarative Agent Languages and Technologies, (DALT), volume 4327 of LNAI, pages 174-190. Springer Verlag, 2006 [pdf].

  • Prova: Rule-based Java Scripting for Distributed Web Applications: A Case Study in Bioinformatics by A. Kozlenkov, R. Penaloza, V. Nigam, L. Royer, G. Dawelbait, and M. Schroeder. In Sebastian Schaffert, editor, Reactivity on the Web at the International Conference on Extending Database Technology (EDBT 2006), volume 4254 of LNCS, pages 899-908, Springer Verlag, 2006 [pdf].

2004

  • Bloco Flexível Matemático by V. Nigam. Revista Controle e Instrumentação, Edition 94. July 2004. Valete Editora Técnica Comercial Ltda., São Paulo, SP [pdf] (in Portuguese).

2003

  • Estudo Comparativo da Aplicação de Técnicas de Inteligência Artificial para a Previsão da Faixa de Peso de Récem-Nascidos by V. Nigam, C.L. Nasciment Jr., and L. F. C. Nascimento. IX Encontro de Iniciação Científica e Pós-Graduação do ITA, 2003 [pdf] (in Portuguese).