• a two-valued logic for properties of strict functional programs allowing partial functions

    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 737
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     a typed program logic lmf for recursive specification and verification is presented. it comprises a strict functional programming language with polymorphic and recursively defined partial functions and polymorphic data types. the logic is two-valued with the equality symbol as only predicate. quantifiers range over the values, which permits inductive proofs of properties. the semantics is based on a contextual (observational) semantics, which gives a consistent presentation of higher-order functions. our analysis also sheds new light on the the role of partial functions and loose specifications. it is also an analysis of influence of extensions of programs on the tautologies. the main result is that universally quantified equations are conservative, which is also the base for several other conservative classes of formulas.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین ژورنال ها