Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Notice bibliographique
Résumé
This volume contains the papers presented at the 4th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2009), held in Montreal, Canada, August 2, 2009. This workshop is the fourth in this series of international meetings, which combines two earlier series: the LFM workshop series on "Logical Frameworks and Meta-Languages" and the MERλIN workshop series on "MEchanized Reasoning about Languages and variable bINding." The previous meetings were held in Pittsburgh, USA in 2008, Bremen, Germany in 2007, and Seattle, USA in 2006. Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their applications on the other have been the focus of considerable research over the last two decades, using competing and sometimes incompatible basic principles. In recent years, there has also been a tremendous amount of work around the POPLMARK challenge, which focuses on mechanizing languages involving binders. This workshop brings together designers, implementers, and practitioners working on these areas. The broad subject areas of LFMTP 2009 are: •the automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation; •the design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology; •theoretical and practical issues concerning the encoding of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures; •case studies of meta-programming, and the mechanization of the (meta) theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory were particularly encouraged. A total of 14 submissions were received in response to the call for papers. Each paper was reviewed by at least three referees and 9 papers were accepted for publication in these proceedings. In addition to the accepted papers, the scientific program included an invited talk given by Gilles Dowek (Ecole Polytechnique and INRIA), and an invited tutorial given by Wilmer Ricciotti (University of Bologna), both joint with the International Workshop on Proof-Search in Type Theories (PSTT).
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction distillée sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Apprise à partir de 10 348 étiquettes directes de Codex et de 10 348 étiquettes directes de Gemma. Le mode candidate est l'union des têtes enseignantes seuillées; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont ni des étiquettes humaines ni des étiquettes directes de modèles de pointe.
Scores Codex et Gemma par catégorie
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,001 | 0,002 |
| Méta-épidémiologie (sens strict) | 0,000 | 0,000 |
| Méta-épidémiologie (sens large) | 0,000 | 0,000 |
| Bibliométrie | 0,000 | 0,000 |
| Études des sciences et des technologies | 0,000 | 0,000 |
| Communication savante | 0,000 | 0,000 |
| Science ouverte | 0,001 | 0,001 |
| Intégrité de la recherche | 0,001 | 0,001 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,000 | 0,000 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule tête enseignante, pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».