تقدم هذه الورقة نهجًا جديدًا للتحقق المعياري في تطوير البرمجيات من خلال دمج منهجية هوار ضمن نظرية الأنواع المعتمدة غير القابلة للتغيير. تتناول القيود المفروضة على طرق التحقق التقليدية، التي تفصل بين التنفيذ والمواصفات دون دعم لغوي للحفاظ على هذا الفصل. يقدم المؤلفون تمييزًا بين المراحل يشفر وظائف التجريد كأنواع، مما يسمح بإنشاء لاصق يربط…

تتناول ورقة البحث التفاعل بين البرمجة الميتا ومعالجات التأثيرات، مع التركيز بشكل خاص على مشكلة استخراج النطاق، مما يؤدي إلى توليد كود غير مناسب. يبرز المؤلفون نهجين لإدارة هذه المشكلة: أنظمة النوع الثابتة، التي تمنع نظريًا استخراج النطاق ولكن تواجه تحديات عملية في التنفيذ، والتحقق الديناميكي، الذي يُستخدم بشكل أكثر شيوعًا في الممارسة (مثل MetaOCaml)…