29 Search Results for "Harper, Robert"

Document
DOI: 10.4230/LIPIcs.CSL.2026.40
The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.39
A Canonical Form for Universe Levels in Impredicative Type Theory

Authors: Yoan Géran

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The 0-imax-successor algebra, where imax: ℕ × ℕ → ℕ is the function defined by imax(n, 0) = 0 and imax(n, S(m)) = max(n, S(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Rocq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.
Cite as

Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{geran:LIPIcs.CSL.2026.39,
  author =	{G\'{e}ran, Yoan},
  title =	{{A Canonical Form for Universe Levels in Impredicative Type Theory}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.39},
  URN =		{urn:nbn:de:0030-drops-254640},
  doi =		{10.4230/LIPIcs.CSL.2026.39},
  annote =	{Keywords: universe levels, canonical form, impredicativity, imax algebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.21
Classifying Covering Types in Homotopy Type Theory

Authors: Samuel Mimram and Émile Oleon

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as the Galois correspondence. In particular, the covering space corresponding to the trivial group is the universal covering, which is a "1-connected" variant of the original space, in the sense that it has the same homotopy groups, except for the first one which is trivial. In this article, we formalize this correspondence in homotopy type theory, a variant of Martin-Löf type theory in which types can be interpreted as spaces (up to homotopy). Along the way, we develop an n-dimensional generalization of covering spaces. Moreover, in order to demonstrate the applicability of our approach, we formally classify the covering of lens spaces and explain how to construct the Poincaré homology sphere.
Cite as

Samuel Mimram and Émile Oleon. Classifying Covering Types in Homotopy Type Theory. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mimram_et_al:LIPIcs.CSL.2026.21,
  author =	{Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Classifying Covering Types in Homotopy Type Theory}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.21},
  URN =		{urn:nbn:de:0030-drops-254456},
  doi =		{10.4230/LIPIcs.CSL.2026.21},
  annote =	{Keywords: homotopy type theory, covering, Galois correspondence}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.7
A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.
Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.11
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

Authors: Jan van Brügge, Andrei Popescu, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Nominal Isabelle provides powerful tools for meta-theoretic reasoning about syntax of logics or programming languages, in which variables are bound. It has been instrumental to major verification successes, such as Gödel’s incompleteness theorems. However, the existing tooling is not compositional. In particular, it does not support nested recursion, linear binding patterns, or infinitely branching syntax. These limitations are fundamental in the way nominal datatypes and functions on them are constructed within Nominal Isabelle. Taking advantage of recent theoretical advancements that overcome these limitations through a modular approach using the concept of map-restricted bounded natural functor (MRBNF), we develop and implement a new definitional package for binding-aware datatypes in Isabelle/HOL, called MrBNF. We describe the journey from the user specification to the end-product types, constants and theorems the tool generates. We validate MrBNF in two formalization case studies that so far were out of reach of nominal approaches: (1) Mazza’s isomorphism between the finitary and the infinitary affine λ-calculus, and (2) the POPLmark 2B challenge, which involves non-free binders for linear pattern matching.
Cite as

Jan van Brügge, Andrei Popescu, and Dmitriy Traytel. Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbrugge_et_al:LIPIcs.ITP.2025.11,
  author =	{van Br\"{u}gge, Jan and Popescu, Andrei and Traytel, Dmitriy},
  title =	{{Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.11},
  URN =		{urn:nbn:de:0030-drops-246091},
  doi =		{10.4230/LIPIcs.ITP.2025.11},
  annote =	{Keywords: syntax with bindings, datatypes, inductive predicates, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.14
Canonical for Automated Theorem Proving in Lean

Authors: Chase Norman and Jeremy Avigad

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic supports higher-order and dependently-typed goals, structural recursion over indexed inductive types, and definitional equality. Canonical finds proofs for 84% of Natural Number Game problems in 51 seconds total.
Cite as

Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
  author =	{Norman, Chase and Avigad, Jeremy},
  title =	{{Canonical for Automated Theorem Proving in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.14},
  URN =		{urn:nbn:de:0030-drops-246128},
  doi =		{10.4230/LIPIcs.ITP.2025.14},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.17
MUSE: Designing Immersive Virtual Realities for Spaceflight UX Research

Authors: Noora Archer, Pasquale Castellano, and Aidan Cowley

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
Virtual reality (VR) provides unique opportunities for assessing early spacecraft design and usability by employing human-centered narrative and scenario-driven design methods. This paper details a narrative-focused VR simulation of a speculative spaceflight scenario, emphasizing narrative techniques for enhancing user immersion and user testing in evaluating operational usability aspects inside a spacecraft capsule. We designed a Modular User-centric Spaceflight Experience (MUSE) including a spacecraft capsule design and virtual mission scenario based on the findings and suggestions in Human Inspirator Co-Engineering (HICE) study. Results from user testing with MUSE underline the effectiveness and opportunities of narrative scenarios in early UX- evaluations in improving experience flow, operational understanding and user engagement. At the same time there remains several questions in defining best methodology to measure users insight and action motivation born from narrative immersion with the VR- experience.
Cite as

Noora Archer, Pasquale Castellano, and Aidan Cowley. MUSE: Designing Immersive Virtual Realities for Spaceflight UX Research. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 17:1-17:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{archer_et_al:OASIcs.SpaceCHI.2025.17,
  author =	{Archer, Noora and Castellano, Pasquale and Cowley, Aidan},
  title =	{{MUSE: Designing Immersive Virtual Realities for Spaceflight UX Research}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{17:1--17:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.17},
  URN =		{urn:nbn:de:0030-drops-240079},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.17},
  annote =	{Keywords: Virtual Reality, Spaceflight Simulation, Narrative Design, Game Design, Scenario Design, Immersive Experience}
}
Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2025.39
Consumable Data via Quantum Communication

Authors: Dar Gilboa, Siddhartha Jain, and Jarrod R. McClean

Published in: LIPIcs, Volume 353, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)

Abstract
Classical data can be copied and re-used for computation, with adverse consequences economically and in terms of data privacy. Motivated by this, we formulate problems in one-way communication complexity where Alice holds some data x and Bob holds m inputs y_1, …, y_m. They want to compute m instances of a bipartite relation R(⋅,⋅) on every pair (x, y_1), …, (x, y_m). We call this the asymmetric direct sum question for one-way communication. We give examples where the quantum communication complexity of such problems scales polynomially with m, while the classical communication complexity depends at most logarithmically on m. Thus, for such problems, data behaves like a consumable resource that is effectively destroyed upon use when the owner stores and transmits it as quantum states, but not when transmitted classically. We show an application to a strategic data-selling game, and discuss other potential economic implications.
Cite as

Dar Gilboa, Siddhartha Jain, and Jarrod R. McClean. Consumable Data via Quantum Communication. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 39:1-39:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gilboa_et_al:LIPIcs.APPROX/RANDOM.2025.39,
  author =	{Gilboa, Dar and Jain, Siddhartha and McClean, Jarrod R.},
  title =	{{Consumable Data via Quantum Communication}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{39:1--39:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.39},
  URN =		{urn:nbn:de:0030-drops-244059},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.39},
  annote =	{Keywords: quantum communication, one-time programs, data markets}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2025.6
Enhancing Creative Thinking Through Gamification in LMS Environments

Authors: Maria João Varanda Pereira, Luís M. Alves, Adina Cocu, Sandra M. Dingli, Montse Meneses, and Ramon Vilanova

Published in: OASIcs, Volume 133, 6th International Computer Programming Education Conference (ICPEC 2025)

Abstract
Gamification in educational context involves applying game design elements and principles to enhance the learning experience. By incorporating the motivational features of games, it aims to engage students and support educational goals. The work presented in this article is part of ThinkGame Erasmus+ project. The project’s goal is to encourage the use of Learning Management System (LMS) tools, such as lessons, wikis, and online tests to create gamified experiences in programming classes. These innovative strategies are intended to boost student motivation and creativity by incorporating compelling narratives, adaptable challenges, collaborative tasks, and continuous feedback. Another important challenge addressed in the project was fostering creativity among teachers, encouraging them to transform conventional, non-gamified resources into engaging and thought-provoking activities for students. A case study composed of ten gamified experiences was developed at Polytechnic Institute of Bragança, one of the project partners, during one semester in Imperative Programming subject.
Cite as

Maria João Varanda Pereira, Luís M. Alves, Adina Cocu, Sandra M. Dingli, Montse Meneses, and Ramon Vilanova. Enhancing Creative Thinking Through Gamification in LMS Environments. In 6th International Computer Programming Education Conference (ICPEC 2025). Open Access Series in Informatics (OASIcs), Volume 133, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{pereira_et_al:OASIcs.ICPEC.2025.6,
  author =	{Pereira, Maria Jo\~{a}o Varanda and Alves, Lu{\'\i}s M. and Cocu, Adina and Dingli, Sandra M. and Meneses, Montse and Vilanova, Ramon},
  title =	{{Enhancing Creative Thinking Through Gamification in LMS Environments}},
  booktitle =	{6th International Computer Programming Education Conference (ICPEC 2025)},
  pages =	{6:1--6:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-393-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{133},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Portela, Filipe and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2025.6},
  URN =		{urn:nbn:de:0030-drops-240369},
  doi =		{10.4230/OASIcs.ICPEC.2025.6},
  annote =	{Keywords: Creative Thinking, Gamification, LMS, Teaching Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.4
Substructural Parametricity

Authors: C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cite as

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aberle_et_al:LIPIcs.FSCD.2025.4,
  author =	{Aberl\'{e}, C. B. and Crary, Karl and Martens, Chris and Pfenning, Frank},
  title =	{{Substructural Parametricity}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.4},
  URN =		{urn:nbn:de:0030-drops-236193},
  doi =		{10.4230/LIPIcs.FSCD.2025.4},
  annote =	{Keywords: Substructural type systems, logical relations, ordered logic}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.5
Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation

Authors: Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.’s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda’s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality.
Cite as

Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami. Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sirman_et_al:LIPIcs.TYPES.2024.5,
  author =	{Sirman, Matthew and Lennon-Bertrand, Meven and Krishnaswami, Neel},
  title =	{{Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.5},
  URN =		{urn:nbn:de:0030-drops-233673},
  doi =		{10.4230/LIPIcs.TYPES.2024.5},
  annote =	{Keywords: Dependent type theory, Bidirectional typing, Observational equality, Normalisation by evaluation}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.9
Complexity of Cubical Cofibration Logics I: coNP-Complete Examples

Authors: Robert Rose and Daniel R. Licata

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete.
Cite as

Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rose_et_al:LIPIcs.TYPES.2024.9,
  author =	{Rose, Robert and Licata, Daniel R.},
  title =	{{Complexity of Cubical Cofibration Logics I: coNP-Complete Examples}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9},
  URN =		{urn:nbn:de:0030-drops-233711},
  doi =		{10.4230/LIPIcs.TYPES.2024.9},
  annote =	{Keywords: cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.20
Incremental Computing by Differential Execution

Authors: Prashant Kumar, André Pacak, and Sebastian Erdweg

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Incremental computing offers the potential for significant performance gains by efficiently updating computations in response to changing data. However, traditional approaches are either problem-specific or use an inefficient all-or-nothing strategy of rerunning affected computations entirely. This paper presents differential semantics, a novel approach that directly embeds the propagation of changes into the semantics of a general-purpose programming language. Given a precise description of input changes, differential semantics rules define how these changes are tracked and propagated through core language constructs like assignments, conditionals, and loops to produce corresponding output changes. We formalize differential semantics and verify key properties, including correctness, using the Rocq proof assistant. We also develop and formally prove a set of optimizations, particularly for loop handling, that enable asymptotic performance improvements. An implementation of the semantics as a differential interpreter achieves order-of-magnitude speedups over recomputation on the Bellman-Ford shortest path algorithm.
Cite as

Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kumar_et_al:LIPIcs.ECOOP.2025.20,
  author =	{Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
  title =	{{Incremental Computing by Differential Execution}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.20},
  URN =		{urn:nbn:de:0030-drops-233137},
  doi =		{10.4230/LIPIcs.ECOOP.2025.20},
  annote =	{Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.3
Pydrofoil: Accelerating Sail-Based Instruction Set Simulators

Authors: Carl Friedrich Bolz-Tereick, Luke Panayi, Ferdia McKeogh, Tom Spink, and Martin Berger

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We present Pydrofoil, a multi-stage compiler that generates instruction set simulators (ISSs) from processor instruction set architectures (ISAs) expressed in the high-level, verification-oriented ISA specification language Sail. Pydrofoil achieves a > 230× speedup over the C-based ISS generated by Sail on our benchmarks, thanks to the following insights. (i) An ISS is effectively an interpreter loop, and tracing just-in-time (JIT) compilers have proven effective at accelerating those, albeit mostly for dynamically typed languages. (ii) ISS workloads are highly atypical, dominated by intensive bit manipulation operations. Conventional compiler optimisations for general-purpose programming languages have limited impact for speeding up such workloads. We develop suitable domain-specific optimisations. (iii) Neither tracing JIT compilers, nor ahead-of-time (AOT) compilation alone, even with domain-specific optimisations, suffice for the generation of performant ISSs. Pydrofoil therefore implements a hybrid approach, pairing an AOT compiler with a tracing JIT built on the meta-tracing PyPy framework. AOT and JIT use domain-specific optimisations. Our benchmarks demonstrate that combining AOT and JIT compilers provides significantly greater performance gains than using either compiler alone.
Cite as

Carl Friedrich Bolz-Tereick, Luke Panayi, Ferdia McKeogh, Tom Spink, and Martin Berger. Pydrofoil: Accelerating Sail-Based Instruction Set Simulators. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 3:1-3:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bolztereick_et_al:LIPIcs.ECOOP.2025.3,
  author =	{Bolz-Tereick, Carl Friedrich and Panayi, Luke and McKeogh, Ferdia and Spink, Tom and Berger, Martin},
  title =	{{Pydrofoil: Accelerating Sail-Based Instruction Set Simulators}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{3:1--3:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.3},
  URN =		{urn:nbn:de:0030-drops-232962},
  doi =		{10.4230/LIPIcs.ECOOP.2025.3},
  annote =	{Keywords: Instruction set architecture, processor, domain-specific language, just-in-time compilation, meta-tracing}
}
  • Refine by Type
  • 29 Document/PDF
  • 18 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 15 2025
  • 1 2024
  • 2 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 6 Harper, Robert
  • 3 Sterling, Jonathan
  • 2 Angiuli, Carlo
  • 2 Cavallo, Evan
  • 2 Gratzer, Daniel
  • Show More...

  • Refine by Series/Journal
  • 26 LIPIcs
  • 2 OASIcs
  • 1 LITES

  • Refine by Classification
  • 13 Theory of computation → Type theory
  • 4 Theory of computation → Denotational semantics
  • 3 Theory of computation → Categorical semantics
  • 3 Theory of computation → Logic and verification
  • 2 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 5 homotopy type theory
  • 2 Dependent type theory
  • 2 Homotopy Type Theory
  • 2 cubical type theory
  • 1 Artin gluing
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact