Literatura cytowana w opisie projektu

[abr96] J-R. Abrial.

The B Book. Assigning meanings to programs. Cambridge University Press, Cambridge, 1996.

[BKMRS77] Banachowski, L., Kreczmar, A., Mirkowska, G., Rasiowa, H. i A. Salwicki.

An introduction to algorithmic logic: mathematical investigations in the theory of programs. Mathematical Foundations of Computer Science, A. Mazurkiewicz i Z. Pawlak (red.). Banach Center Publications, Warszawa, PWN 1977.

[bmv95] Basin, D., Matthews, S., L.Vigano.

A modular presentation of modal logics in a logical framework. Proc. 1st Isabelle User Workshop, pp.137--148, Cambridge, 1995.

[bed95-opis] M. A. Bednarczyk.

Logic of predicetes versus linear logic. Prace IPI PAN 795, Warszawa 1995.

[bb95-opis] M. A. Bednarczyk i T. Borzyszkowski.

Towards program development, specification and verification with Isabelle. Proc. of the First Isabelle Users Workshop'95, Cambridge, pp.101--121, 1995.

[bed96-opis] M. A. Bednarczyk.

Logic of predicates with explicit substitutions. Mathematical Foundations of Computer Science 1996, 21th International Symposium, Cracow, Poland, Proceedings (eds. W. Penczek & A. Szalas), LNCS 1113, 192-206, 1996.

[bb96-opis] Bednarczyk, M. A., T. Borzyszkowski.

Information system development as mechanizable logical activity. Information System Development --- ISD'96, 5th International Conference, Gdańsk, Poland, Proceedings (eds. S. Wrycza & J. Zupancic), 535-544, 1996.

[bcetc90] Burch, J.R., Clarke, E.M., McMillan, K.L, Dill, D. L. i J. Hwang.

Symbolic model checking 10^{20} states and beyond. Proc. LICS'90, str. 428-439, 1990.

[ces86] Clarke, E.M., Emerson, E. A. i A. P. Sistala.

Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Trans. on Progr. Languages & Systems, 8, str. 244-263, 1986.

[dij76] Dijkstra, E.

A Discipline of Programming. Prentice-Hall, 1976.

[ds90] Dijkstra, E. i C. S. Scholten.

Predicate Calculus and Program Semantics. Springer, 1990.

[djlm94a] B. Dunin-Kęplicz, J. Jabłonowski, W. Łukaszewicz i E. Madalińska-Bugaj.

Developing programs from specifications: design of the system. 3rd Information System Development Workshop'92, 145--168, 1992.

[djlm94b] B. Dunin-Kęplicz, J. Jabłonowski, W. Łukaszewicz i E. Madalińska-Bugaj.

CAProDel: a system for Computer Aided Program Development. 6th Software Engineering and Knowledge Engineering Conference, SEKE'94, Jurmala, 470--477, 1994.

[gab94] Gabbay, D.

Labelled Deductive Systems. Part 1 --- Foundations. Max-Planck-Institut für Informatik, Research Report MPI-I-223-94,1994.

[gor89] M. Gordon.

Mechanizing programing logics in Higher Order Logic. In G. Birtwistle and P. A. Subrahmanyam (ed's) Current Trends in Hardware Verification and Automated Theorem Proving, Springer, 1989.

[GP94] M. Gordon i A. Pitts.

The HOL Logic and System. In J. Bowen(ed.) Proc. Towards Verified Systems, Elsevier, Real-Time Safety Critical Systems, series, 1994.

[Har79] Harel, D.

First order dynamic logic. Lecture Notes in Computer Science, vol. 68, Springer, 1979.

[hm94] Honsell, F., M. Miculan.

A Natural Deduction approach to Program Logics. Technical Report, University of Pisa, 1994.

[hoa69] Hoare, C.A.R.

An axiomatic basis for computer programming. Communications of the ACM, 12(10), pp.576--583, 1969.

[kst94] S. Kahrs, D. Sannella i A. Tarlecki.

The definition of Extended ML: a gentle introduction. Theoretical Computer Science, ukaże się.

[krytenko97] A. Krytenko.

Konstrukcja algorytmu Euklidesa. Praca magisterska, Instytut Matematyki Uniwersytetu Gdańskiego, 1997.

[lin95] Lin, H.

On implementing unique fixpoint induction for value-passing processes. Proceedings TACAS'95 Workshop, Århus, 1995.

[lin96] Lin, H.

Symbolic graphs with assignment. Proceedings CONCUR'96, Pisa, LNCS 1119, str. 50--65, Springer, 1996.

[MartinLoef] P. Martin-Löf.

An intuitionistic theory of types: predicative part. In Logic Colloquium'73, str. 73--118, Noth-Holland, 1975.

[Mil78] Milner R.

A theory of type polymorphism in programming. J. Comp. Sys. Sci. 17, pp. 348--375, 1978.

[MS92] Mirkowska, G. i A. Salwicki.

Logika algorytmiczna dla programistów. Warszawa, WNT, 1992.

[old91] E-R. Olderog.

Nets, Terms & Formulas. Cambridge University Press, Cambridge, 1991.

[Isabelle] L. C. Paulson.

Isabelle: a Generic Theorem Prover. (with contributions by T. Nipkow). LNCS 828, Springer, 1994.

[nwpt95-opis] P. Pączkowski,

Verifying CBS processes using symbolic bisimulation, Proc. 7th Nordic Workshop on Programming Theory (B. Bjerner, M. Larsson, B. Nordstrom, eds.), PMG Report 86, Goteborg University and Chalmers University of Technology, str. 310--323, 1996.

[infinity96-opis] P. Pączkowski,

Characterizing bisimilarity of value-passing parametrised processes, INFINITY, International Workshop on Verification of Infinite State Systems, (B. Stefffen and T. Margaria, Eds.), str. 47--55, MIP-9614, Universität Passau, 1996 (pełna wersja ukaże się w Electronic Notes of TCS).

[pps96-opis] W. Pawłowski, P. Pączkowski, S. Sokołowski,

Specifying and Verifying Parametric Processes. Proceedings of MFCS'96, (W. Penczek, A. Szałas, Eds.), LNCS 1113, Springer-Verlag, 1996.

[rh96] Rathke, J. i M. Hennessy.

Local model checking for a value-based modal µ-calculus. Raport techniczny Uniwersytetu Sussex, 5/96, 1996.

[sst92-opis] D. Sannella, S. Sokołowski i A. Tarlecki.

Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica 29, 689--736, 1992.

[st95] D. Sannella i A. Tarlecki.

Model-theoretic foundations for formal development: basic concepts and motivations. Prace IPI PAN 791, Warszawa 1995. (Rozszerzenie wcześniejszej pracy tych samych autorów: Toward formal development of programs from algebraic specifications: model-theoretic foundations. Proc 19th ICALP'92, Vienna, LNCS 623, 656--671, Springer, 1992).

[sok88-opis] Sokołowski S. Soundness of Hoare's logic: an automated proof using LCF.

TOPLAS 9, 100--120, 1987.

[SW95] Sokołowski S., Wadler P.

Hindley-Milner for dependent and subset types. In Proc. 7th Nordic Workshop on Programming Theory, Göteborg, Sweden, 1--3 November 1995 (Bror Bjerner, Marie Larsson, Bengt Nordström eds.), pp. 438--453.