-
strongly typed term representations in coq
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 949
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
there are two approaches to formalizing the syntax of typed object languages in a proof assistant or programming language. the extrinsic approach is to first define a type that encodes untyped object expressions and then make a separate definition of typing judgements over the untyped terms. theintrinsic approach is to make a single definition that captures well-typed object expressions, so ill-typed expressions cannot even be expressed. intrinsic encodings are attractive and naturally enforce the requirement that metalanguage operations on object expressions, such as substitution, respect object types. the price is that the metalanguage types of intrinsic encodings and operations involve non-trivial dependency, adding significant complexity. this paper describes intrinsic-style formalizations of both simply-typed and polymorphic languages, and basic syntactic operations thereon, in the coq proof assistant. the coq types encoding object-level variables (de bruijn indices) and terms are indexed by both type and typing environment. one key construction is the boot-strapping of definitions and lemmas about the action of substitutions in terms of similar ones for a simpler notion of renamings. in the simply-typed case, this yields definitions that are free of any use of type equality coercions. in the polymorphic case, some substitution operations do still require type coercions, which we at least partially tame by uniform use of heterogeneous equality.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
بررسی تأثیر برنامه ریزی منابع سازمانی بر چابکی و اثربخشی سازمانی (مورد مطالعه: اداره کل آموزش و پرورش استان سیستان و بلوچستان)
-
بهینه یابی سطح لغزش بحرانی شیب های خاکی مسلح به روش قطعات افقی
-
استفاده از نشانه های کمک دیداری در محیط آموزشی به منظور یادگیری بهتر کودکان اوتیستیک
-
بررسی کیفیت فضای بازی در ساختمان های تجاری با رویکرد ارتقاء تحرک کودکان
-
تولید یک کلون از یاخته های پایدار کلیه گوساله و ارزیابی حساسیت آن در برابر ویروس های پاراآنفولانزا تیپ سه و هرپس سیمپلکس تیپ یک
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
امکان ایجاد مزیت رقابتی با بهره گیری از عملکردهای زیست محیطی-اقتصادی و اجتماعی با حمایت مدیران میانی و عالی و اتخاذ استراتژی
-
بررسی تاثیر فشارهای اجتماعی، تعهد و ویژگی های شخصیتی بر قضاوت حسابرسان
-
بررسی وضعیت سلامت معنوی در کارکنان یکی از دانشگاه های علوم پزشکی شهر تهران
-
بررسی باغ شهر شیراز در دوره صفوی بر اساس دو عنصر باغ محور و میدان
-
تاب آوری زنجیره تامین در شرایط کرونا
سوال خود را در مورد این مقاله مطرح نمایید :