Publications and drafts
V. Komendantsky.
Reflexive toolbox for regular expression matching:
Verification of functional programs in Coq+Ssreflect.
In Proceedings of the 6th ACM SIGPLAN Workshop
Programming Languages meets Program Verification,
PLPV 2012, 24 January 2012,
Philadelphia, USA. ACM.
[full text]
[Coq proofs]
V. Komendantsky.
Subtyping by folding an inductive relation into a coinductive one.
In Post-proceedings of the 12th International Symposium on Trends
in Functional Programming, TFP
2011, Madrid, Spain, 16-18 May 2011. LNCS, Springer.
[full text]
[Coq proofs]
V. Komendantsky.
Packed views of pre-structured data.
Extended abstract. In Workshop on Computer Theorem Proving Components
for Educational Software,
THedu 2011,
Wroclaw, Poland, 31 July 2011.
[full text]
V. Komendantsky.
Regular expression containment as a proof search problem.
In Pre-proceedings of the International Workshop on
Proof-Search in Axiomatic Theories and Type Theories,
PSATTT
2011, Wroclaw, Poland, 1 August 2011.
[full text]
V. Komendantsky.
Application of monadic substitution to recursive type containment.
In Pre-proceedings of the 10th International Workshop on Reduction Strategies in
Rewriting and Programming,
WRS 2011,
Novi Sad, Serbia, 29 May 2011.
[full text]
V. Komendantsky.
Subtyping by folding an inductive relation into a coinductive one.
In Pre-proceedings of the 12th International Symposium on Trends
in Functional Programming, TFP
2011, Madrid, Spain, 16-18 May 2011. (Superceeded by the extended
post-proceedings version.)
[full text]
[Coq proofs]
V. Komendantsky.
Computable partial derivatives of regular expressions.
Draft. 2011.
[full text]
[Coq proofs]
V. Komendantsky, A. Konovalov and S. Linton.
View of computer algebra data from Coq.
In Proc. Conference on Intelligent Computer
Mathematics, CICM 2011,
Bertinoro, Forli, Italy, 18-23 July 2011. LNAI.
[full text]
[Coq plugin]
V. Komendantsky, A. Konovalov and S. Linton.
Interfacing Coq + SSReflect with GAP.
In Proc. User Interfaces for Theorem Provers,
UITP 2010.
Edinburgh, Scotland, 15 July 2010. Editors D. Aspinall and C. Sacerdoti
Coen. ENTCS, Elsevier.
[full text]
V. Komendantsky and A. K. Seda. Neural Networks and Minimal Fixed Point Semantics for Logic Programs. Proc. Information '09. 6-9 November, 2009, Kyoto University, Kyoto, Japan.
V. Komendantsky.
Case analysis on a dependently typed fixed point for
regular languages.
YesLogic technical report. July 2009.
[full text]
M. Day and V. Komendantsky.
A compiler of regular expressions to NFAs.
YesLogic technical report.
May 2009.
[full text]
V. Komendantsky.
Denotational semantics of call-by-name
normalization in lambda-mu calculus.
Electronic Notes in Theoretical Computer
Science, volume 225, pages 161-179, 2009.
[full text]
Y. Bertot and V. Komendantsky.
Fixed point semantics and partial recursion in Coq.
Proc. 10th Intl ACM SIGPLAN Symposium on Principles and
Practice of Declarative Programming (PPDP'08),
Valencia, Spain, 15-17 July, 2008, pages 89-96.
[full text]
[Coq plugin]
[Coq proofs]
E. Komendantskaya and V. Komendantsky.
On uniform proof-theoretical operational semantics for logic
programming.
In J.-Y. Beziau and A.Costa-Leite, editors, Perspectives on
Universal Logic, pages 379-394. Polimetrica Publisher, 2007.
[full text]
Li, Ren, Hurley, Komendantsky, Mac an Airchinnigh, Schellekens, Seda, Strong and Woods. Proc. Information-MFCSIT 2006, 1st-5th August, 2006. UCC Press, Cork. ISBN-10: 0-9552229-3-1.
V. Komendantsky.
Categorical semantics of normalization in lambda-C calculus.
In Proc. Information-MFCSIT 2006, 1st-5th August, 2006. UCC
Press, Cork. pages 233-236.
[full text]
V. Komendantsky and A. K. Seda.
Computation of normal logic programs by fibring neural networks.
In Proc. 7th International Workshop on First-Order Theorem
Proving (FTP'05), pages 97-111, Koblenz, Germany, September 15-17,
2005.
[full text]
E. Komendantskaya, A. K. Seda, and V. Komendantsky.
On approximation of the semantic operators determined by
bilattice-based logic programs.
In Proc. 7th International Workshop on First-Order Theorem
Proving (FTP'05), pages 112-130, Koblenz, Germany, September 15-17,
2005.
[full text]
V. Komendantsky.
Theory of inference in many-valued logics. PhD thesis. Institute of
Philosophy, Russian Academy of Sciences, 23 October, 2003. In Russian.
[English abstract]
[Russian autoreferat]
V. Komendantsky. Priestley representation theorem and resolution method in many-valued logics. In Logicheskiye Issledovaniya, volume 10. Nauka, Moscow, 2003. 16 pages.
V. Komendantsky. On automated theorem proving by means of representation theory in Lukasiewicz logics. In Proc. IV Intl. Conf. Smirnov Readings, pages 78-79, Moscow, May 2003. IPh RAS.
V. Komendantsky. Method of resolution in mixed Post logic. In Proc. Seminar of the IPh RAS logic centre, volume XVI, pages 64-74. IPh RAS, Moscow, 2002.
V. Komendantsky.
Resolution for mixed Post logic.
In Proc. 4th ESSLLI Student Session, Trento, Italy, August
2002. University of Trento. 11 pages.
[full text]
V. Komendantsky. On a game semantics for infinite-valued Lukasiewicz logic. In Contemporary logic: problems of its theory, history, and scientific applications. Proc. VII All-Russian Conf. Saint-Petersburg State University, June 2002.
V. Komendantsky. OTTER and a proof of implication reflexivity. In Proc. Seminar of the IPh RAS logic centre, volume XV, pages 57-60. IPh RAS, Moscow, 2001.
V. Komendantsky. Ignorance in logics of knowledge. In Smirnov Readings. III Intl. Conf., page 245, Moscow, May 2001. IPh RAS.
V. Komendantsky. 3-valued isomorphs of classical logic. In Contemporary logic: problems of its theory, history, and scientific applications. Proc. VI All-Russian Conf. Saint-Petersburg State University, June 2000.