Ing. Ondřej Ryšavý, Ph.D.

Dependent type system for object-oriented programming languages
Reseach leader:Kolář Dušan, Škarvada Libor
Team leaders:Peterka Ondřej, Ryšavý Ondřej
Agency:GAČR
Code:GA201/09/1316
Start:2009
End:2009
Files: 
Soubor /proj/355/201-09-1316_pcz.pdf nemáte právo číst:
doc_folder_proj1: /proj/355/201-09-1316_pcz.pdf no access 3
Keywords:

dependent types; formal reasoning; functional programming; lambda calculus; language constructs and features; object calculus; object orientation; program specification and verification; type theory;

Annotation:
Advanced type systems can provide more safety than type systems of programming languages currently in use. Moreover, they can change the style of programming discipline if used rigorously. The proposed project aims at basic research of a new type system for object-oriented programming languages that allows to guarantee safer programs, type check more language constructs and support the correct-by-construction development and implementation methodology. The contribution of the project comes with its approach. Shortly, we plan to emit functional programming with dependent types into the object-oriented environment and investigate the possible incidences. In particular, the dependent types in subtyping imposed by class-based inheritance as the basic concept for reuse and modularity, and the relation with traditional lambda-based theory are two main topics that will be studied. An important part of the project is the development of an experimental language featuring studied principles.

Publications

2009Kollár Matej, Peterka Ondřej, Ryšavý Ondřej, Škarvada Libor: A Calculus of Coercive Subtyping, Brno, CZ, MUNI, 2009, p. 17
 Škarvada Libor, Peterka Ondřej, Ryšavý Ondřej, Kolář Dušan: A Calculus of Coercive Subtyping, In: Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages, South Orange, US, SHU, 2009, p. 182-192

Your IPv4 address: 54.242.233.11
Switch to IPv6 connection

DNSSEC [dnssec]