Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Bibliographic record
Abstract
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).
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.009 | 0.012 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.002 | 0.002 |
| Science and technology studies | 0.002 | 0.005 |
| Scholarly communication | 0.013 | 0.014 |
| Open science | 0.003 | 0.007 |
| Research integrity | 0.004 | 0.008 |
| Insufficient payload (model declined to judge) | 0.058 | 0.015 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".