Le langage CP récemment proposé adopte la programmation compositionnelle : un nouveau style de programmation modulaire qui résout des problèmes difficiles tels que le problème d'expression. Le CP est mis en œuvre au-dessus d'un langage de base polymorphe avec des types d'intersection disjoints appelés Fi+. La sémantique de Fi+ utilise une élaboration vers un langage cible et s'appuie sur une technique de preuve sophistiquée pour prouver la cohérence de l'élaboration. Malheureusement, la technique de preuve est techniquement difficile et difficile à adapter à de nombreuses caractéristiques communes, y compris le polymorphisme récursif ou prédictif. Ainsi, la formulation originale de Fi+ ne prend pas en charge les deux caractéristiques ultérieures, ce qui crée un fossé entre la théorie et la pratique, car la PC s'appuie fondamentalement sur elles. Cet article présente une nouvelle formulation de Fi+ basée sur une sémantique opérationnelle dirigée par type (TDOS). L'approche TDOS a récemment été proposée pour modéliser la sémantique des langages avec des types d'intersection disjoints (mais sans polymorphisme). Nos travaux montrent que l'approche TDOS peut être étendue aux langages à polymorphisme disjoint et modéliser le calcul complet Fi+. Contrairement à la sémantique d'élaboration, qui donne la sémantique à Fi+ indirectement via un langage cible, l'approche TDOS donne une sémantique à Fi+ directement. Avec un TDOS, il n'y a pas besoin de preuve de cohérence. Au lieu de cela, nous pouvons simplement prouver que la sémantique est déterministe. La preuve du déterminisme n'utilise que des techniques de raisonnement simples, telles que l'induction directe, et est capable de gérer des caractéristiques problématiques telles que la récursivité et le polymorphisme impédicatif. Cela supprime le fossé entre la théorie et la pratique et valide les preuves originales de l'exactitude pour la PC. Nous avons formalisé la variante TDOS du calcul Fi+ et toutes ses preuves dans l'assistant de preuve Coq.

El lenguaje CP recientemente propuesto adopta la Programación Composicional: un nuevo estilo de programación modular que resuelve problemas desafiantes como el Problema de Expresión. CP se implementa sobre un lenguaje central polimórfico con tipos de intersección disjuntos llamados Fi+. La semántica de Fi+ emplea una elaboración a un idioma de destino y se basa en una sofisticada técnica de prueba para demostrar la coherencia de la elaboración. Desafortunadamente, la técnica de prueba es técnicamente desafiante y difícil de escalar a muchas características comunes, incluida la recursividad o el polimorfismo impredicativo. Por lo tanto, la formulación original de Fi+ no admite las dos características posteriores, lo que crea una brecha entre la teoría y la práctica, ya que la PC se basa fundamentalmente en ellas. Este documento presenta una nueva formulación de Fi+ basada en una semántica operativa dirigida por tipo (TDOS). Recientemente se propuso el enfoque TDOS para modelar la semántica de los lenguajes con tipos de intersección disjunta (pero sin polimorfismo). Nuestro trabajo muestra que el enfoque TDOS se puede extender a idiomas con polimorfismo disjunto y modelar el cálculo Fi+ completo. A diferencia de la semántica de elaboración, que da la semántica a Fi+ indirectamente a través de una lengua de destino, el enfoque TDOS da una semántica a Fi+ directamente. Con un TDOS, no hay necesidad de una prueba de coherencia. En cambio, podemos simplemente probar que la semántica es determinista. La prueba del determinismo solo utiliza técnicas de razonamiento simples, como la inducción directa, y es capaz de manejar características problemáticas como la recursividad y el polimorfismo impredicativo. Esto elimina la brecha entre la teoría y la práctica y valida las pruebas originales de corrección para la PC. Formalizamos la variante TDOS del cálculo Fi+ y todas sus pruebas en el asistente de pruebas Coq.

The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+. The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of Fi+ does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of Fi+ based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full Fi+ calculus. Unlike the elaboration semantics, which gives the semantics to Fi+ indirectly via a target language, the TDOS approach gives a semantics to Fi+ directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the Fi+ calculus and all its proofs in the Coq proof assistant.

تتبنى لغة حماية الطفل المقترحة مؤخرًا البرمجة التركيبية: أسلوب برمجة معياري جديد يحل المشكلات الصعبة مثل مشكلة التعبير. يتم تنفيذ حماية الطفل على رأس لغة أساسية متعددة الأشكال مع أنواع تقاطع منفصلة تسمى FI+. تستخدم دلالات Fi+ تفصيلاً للغة الهدف وتعتمد على تقنية إثبات متطورة لإثبات تماسك التفصيل. لسوء الحظ، فإن تقنية الإثبات صعبة من الناحية الفنية ويصعب قياسها إلى العديد من السمات المشتركة، بما في ذلك العودية أو تعدد الأشكال المانع. وبالتالي، فإن الصيغة الأصلية لـ FI+ لا تدعم السمتين اللاحقتين، مما يخلق فجوة بين النظرية والتطبيق، لأن حماية الطفل تعتمد عليهما بشكل أساسي. تقدم هذه الورقة صياغة جديدة لـ FI+ بناءً على دلالات تشغيلية موجهة بالنوع (TDOS). تم اقتراح نهج TDOS مؤخرًا لنمذجة دلالات اللغات ذات أنواع التقاطع المنفصلة (ولكن بدون تعدد الأشكال). يُظهر عملنا أنه يمكن توسيع نهج TDOS ليشمل اللغات ذات الأشكال المتعددة المنفصلة ونمذجة حساب التفاضل والتكامل الكامل. على عكس دلالات التفصيل، التي تعطي دلالات لـ Fi+ بشكل غير مباشر عبر لغة مستهدفة، فإن نهج TDOS يعطي دلالات لـ Fi+ مباشرة. مع TDOS، ليست هناك حاجة لإثبات التماسك. بدلاً من ذلك، يمكننا ببساطة إثبات أن الدلالات حتمية. يستخدم إثبات الحتمية فقط تقنيات التفكير البسيطة، مثل الاستقراء المباشر، وهو قادر على التعامل مع السمات الإشكالية مثل العودية وتعدد الأشكال المعيب. هذا يزيل الفجوة بين النظرية والتطبيق ويتحقق من صحة البراهين الأصلية لصحة حماية الطفل. لقد قمنا بإضفاء الطابع الرسمي على متغير TDOS لحساب التفاضل والتكامل FI+ وجميع براهينه في مساعد إثبات COQ.