INRIA, France
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, 2013 – PPDP
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems that are commonly presented via syntax-directed rules that make use of contexts and side-conditions. The two-level logic approach, as ...
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Oretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, vol. 6255,2010 – International Colloquium on Theoretical Aspects of Computing
Model checking has proved to be an efficient technique for finding subtle bugs in concurrent and distributed algorithms and systems. However, it is usually limited to the analysis of small instances of such systems, due to the problem of state space ...
Olivier Savary Belanger, Kaustuv Chaudhuri
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014 – LFMTP
Hypothetical judgments go hand-in-hand with higher-order abstract syntax for meta-theoretic reasoning. The dynamic assumptions of these judgments often have a simple regular structure of repetitions of related assumptions; reflecting on this regular ...
Kaustuv Chaudhuri, Nicolas Guenot
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014 – LICS
The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the ...
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Automated Reasoning, 5th International Joint Conference, IJCAR 2010, vol. 6173,2010 – IJCAR
TLAPS, the TLA + proof system, is a platform for the development and mechanical verification of TLA + proofs. The TLA + proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. ...
Kaustuv Chaudhuri, Frank Pfenning
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, vol. 3632,2005 – CADE
Abstract. We present the theory and implementation of a theorem prover forfirst-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the prover concern resource management andfocused ...