16 Search Results for "Pinto, Luís"

Volume

LIPIcs, Volume 130

24th International Conference on Types for Proofs and Programs (TYPES 2018)

TYPES 2018, June 18-21, 2018, Braga, Portugal

Editors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Document
DOI: 10.4230/OASIcs.ICPEC.2023.3
LCSMAR, an AR Based Tool to Inspect Imperative Programs

Authors: Luis Carlos Martins, Lázaro Vinicius Lima, and Pedro Rangel Henriques

Published in: OASIcs, Volume 112, 4th International Computer Programming Education Conference (ICPEC 2023)

Abstract
LCSMAR is a Learning Resource that takes advantage of Augmented Reality in order to promote the development of Computational Thinking among students who are starting to dive in to the world of computer programming. Students can write code in a imperative programming language and, with the help of their mobile phone, they can visualize and analyze the execution of the code they developed, seeing how variable and data structures change over time with each instruction. Augmented Reality tools allow the visualization of abstract concepts that are often misunderstood and that cause misconception among students, which in term should help students develop the abilities to understand and use these abstract concepts, such as data structures, in other areas of application.
Cite as

Luis Carlos Martins, Lázaro Vinicius Lima, and Pedro Rangel Henriques. LCSMAR, an AR Based Tool to Inspect Imperative Programs. In 4th International Computer Programming Education Conference (ICPEC 2023). Open Access Series in Informatics (OASIcs), Volume 112, pp. 3:1-3:9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{martins_et_al:OASIcs.ICPEC.2023.3,
  author =	{Martins, Luis Carlos and Lima, L\'{a}zaro Vinicius and Henriques, Pedro Rangel},
  title =	{{LCSMAR, an AR Based Tool to Inspect Imperative Programs}},
  booktitle =	{4th International Computer Programming Education Conference (ICPEC 2023)},
  pages =	{3:1--3:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-290-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{112},
  editor =	{Peixoto de Queir\'{o}s, Ricardo Alexandre and Teixeira Pinto, M\'{a}rio Paulo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2023.3},
  URN =		{urn:nbn:de:0030-drops-184994},
  doi =		{10.4230/OASIcs.ICPEC.2023.3},
  annote =	{Keywords: Augmented Reality, Learning Resources, Computer Programming, Computational Thinking}
}
Document
Short Paper
DOI: 10.4230/OASIcs.ICPEC.2023.11
Automated Assessment of Simple Web Applications (Short Paper)

Authors: Luís Maia Costa, José Paulo Leal, and Ricardo Queirós

Published in: OASIcs, Volume 112, 4th International Computer Programming Education Conference (ICPEC 2023)

Abstract
Web programming education is an important component of modern computer science curricula. Assessing students’ web programming skills can be time-consuming and challenging for educators. This paper introduces Webpal, an automated assessment tool for web programming exercises in entry-level courses. Webpal evaluates web applications coded in HTML, CSS, and Javascript, and provides feedback to students. This tool integrates with Virtual Learning Environments (VLEs) through an API, allowing the creation, storage, and access to exercises while assessing student attempts based on the created exercises. The evaluation process comprises various subcomponents: static assessment, interface matching, functional testing, and feedback management. This approach aims to provide feedback that helps students overcome their challenges in web programming assignments. This paper also presents a demo showcasing the tool’s features and functionality in a simulated VLE environment.
Cite as

Luís Maia Costa, José Paulo Leal, and Ricardo Queirós. Automated Assessment of Simple Web Applications (Short Paper). In 4th International Computer Programming Education Conference (ICPEC 2023). Open Access Series in Informatics (OASIcs), Volume 112, pp. 11:1-11:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{costa_et_al:OASIcs.ICPEC.2023.11,
  author =	{Costa, Lu{\'\i}s Maia and Leal, Jos\'{e} Paulo and Queir\'{o}s, Ricardo},
  title =	{{Automated Assessment of Simple Web Applications}},
  booktitle =	{4th International Computer Programming Education Conference (ICPEC 2023)},
  pages =	{11:1--11:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-290-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{112},
  editor =	{Peixoto de Queir\'{o}s, Ricardo Alexandre and Teixeira Pinto, M\'{a}rio Paulo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2023.11},
  URN =		{urn:nbn:de:0030-drops-185072},
  doi =		{10.4230/OASIcs.ICPEC.2023.11},
  annote =	{Keywords: Web Applications, Static Assessment, Interface Matching, Functional Assessment, Feedback Manager}
}
Document
DOI: 10.4230/OASIcs.SLATE.2021.7
MUAHAH: Taking the Most out of Simple Conversational Agents

Authors: Leonor Llansol, João Santos, Luís Duarte, José Santos, Mariana Gaspar, Ana Alves, Hugo Gonçalo Oliveira, and Luísa Coheur

Published in: OASIcs, Volume 94, 10th Symposium on Languages, Applications and Technologies (SLATE 2021)

Abstract
Dialog engines based on multi-agent architectures usually select a single agent, deemed to be the most suitable for a given scenario or for responding to a specific request, and disregard the answers from all of the other available agents. In this work, we present a multi-agent plug-and-play architecture that: (i) enables the integration of different agents; (ii) includes a decision maker module, responsible for selecting a suitable answer out of the responses of different agents. As usual, a single agent can be chosen to provide the final answer, but the latter can also be obtained from the responses of several agents, according to a voting scheme. We also describe three case studies in which we test several agents and decision making strategies; and show how new agents and a new decision strategy can be easily plugged in and take advantage of this platform in different ways. Experimentation also confirms that considering several agents contributes to better responses.
Cite as

Leonor Llansol, João Santos, Luís Duarte, José Santos, Mariana Gaspar, Ana Alves, Hugo Gonçalo Oliveira, and Luísa Coheur. MUAHAH: Taking the Most out of Simple Conversational Agents. In 10th Symposium on Languages, Applications and Technologies (SLATE 2021). Open Access Series in Informatics (OASIcs), Volume 94, pp. 7:1-7:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{llansol_et_al:OASIcs.SLATE.2021.7,
  author =	{Llansol, Leonor and Santos, Jo\~{a}o and Duarte, Lu{\'\i}s and Santos, Jos\'{e} and Gaspar, Mariana and Alves, Ana and Gon\c{c}alo Oliveira, Hugo and Coheur, Lu{\'\i}sa},
  title =	{{MUAHAH: Taking the Most out of Simple Conversational Agents}},
  booktitle =	{10th Symposium on Languages, Applications and Technologies (SLATE 2021)},
  pages =	{7:1--7:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-202-0},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{94},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Sim\~{o}es, Alberto and Portela, Filipe and Pereira, Maria Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2021.7},
  URN =		{urn:nbn:de:0030-drops-144248},
  doi =		{10.4230/OASIcs.SLATE.2021.7},
  annote =	{Keywords: Dialog systems, question answering, information retrieval, multi-agent}
}
Document
DOI: 10.4230/OASIcs.SLATE.2021.8
NER in Archival Finding Aids

Authors: Luís Filipe Costa Cunha and José Carlos Ramalho

Published in: OASIcs, Volume 94, 10th Symposium on Languages, Applications and Technologies (SLATE 2021)

Abstract
At the moment, the vast majority of Portuguese archives with an online presence use a software solution to manage their finding aids: e.g. Digitarq or Archeevo. Most of these finding aids are written in natural language without any annotation that would enable a machine to identify named entities, geographical locations or even some dates. That would allow the machine to create smart browsing tools on top of those record contents like entity linking and record linking. In this work we have created a set of datasets to train Machine Learning algorithms to find those named entities and geographical locations. After training several algorithms we tested them in several datasets and registered their precision and accuracy. These results enabled us to achieve some conclusions about what kind of precision we can achieve with this approach in this context and what to do with the results: do we have enough precision and accuracy to create toponymic and anthroponomic indexes for archival finding aids? Is this approach suitable in this context? These are some of the questions we intend to answer along this paper.
Cite as

Luís Filipe Costa Cunha and José Carlos Ramalho. NER in Archival Finding Aids. In 10th Symposium on Languages, Applications and Technologies (SLATE 2021). Open Access Series in Informatics (OASIcs), Volume 94, pp. 8:1-8:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{costacunha_et_al:OASIcs.SLATE.2021.8,
  author =	{Costa Cunha, Lu{\'\i}s Filipe and Ramalho, Jos\'{e} Carlos},
  title =	{{NER in Archival Finding Aids}},
  booktitle =	{10th Symposium on Languages, Applications and Technologies (SLATE 2021)},
  pages =	{8:1--8:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-202-0},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{94},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Sim\~{o}es, Alberto and Portela, Filipe and Pereira, Maria Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2021.8},
  URN =		{urn:nbn:de:0030-drops-144257},
  doi =		{10.4230/OASIcs.SLATE.2021.8},
  annote =	{Keywords: Named Entity Recognition, Archival Descriptions, Machine Learning, Deep Learning}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2021.10
Automated Java Challenges' Security Assessment for Training in Industry - Preliminary Results

Authors: Luís Afonso Casqueiro, Tiago Espinha Gasiba, Maria Pinto-Albuquerque, and Ulrike Lechner

Published in: OASIcs, Volume 91, Second International Computer Programming Education Conference (ICPEC 2021)

Abstract
Secure software development is a crucial topic that companies need to address to develop high-quality software. However, it has been shown that software developers lack secure coding awareness. In this work, we use a serious game approach that presents players with Java challenges to raise Java programmers' secure coding awareness. Towards this, we adapted an existing platform, embedded in a serious game, to assess Java secure coding exercises and performed an empirical study. Our preliminary results provide a positive indication of our solution’s viability as a means of secure software development training. Our contribution can be used by practitioners and researchers alike through an overview on the implementation of automatic security assessment of Java CyberSecurity Challenges and their evaluation in an industrial context.
Cite as

Luís Afonso Casqueiro, Tiago Espinha Gasiba, Maria Pinto-Albuquerque, and Ulrike Lechner. Automated Java Challenges' Security Assessment for Training in Industry - Preliminary Results. In Second International Computer Programming Education Conference (ICPEC 2021). Open Access Series in Informatics (OASIcs), Volume 91, pp. 10:1-10:11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{casqueiro_et_al:OASIcs.ICPEC.2021.10,
  author =	{Casqueiro, Lu{\'\i}s Afonso and Gasiba, Tiago Espinha and Pinto-Albuquerque, Maria and Lechner, Ulrike},
  title =	{{Automated Java Challenges' Security Assessment for Training in Industry - Preliminary Results}},
  booktitle =	{Second International Computer Programming Education Conference (ICPEC 2021)},
  pages =	{10:1--10:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-194-8},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{91},
  editor =	{Henriques, Pedro Rangel and Portela, Filipe and Queir\'{o}s, Ricardo 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.2021.10},
  URN =		{urn:nbn:de:0030-drops-142269},
  doi =		{10.4230/OASIcs.ICPEC.2021.10},
  annote =	{Keywords: Education, Teaching, Training, Awareness, Secure Coding, Industry, Programming, Cybersecurity, Capture-the-Flag, Intelligent Coach}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.4
Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic

Authors: José Espírito Santo, Ralph Matthes, and Luís Pinto

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
Cite as

José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s},
  title =	{{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4},
  URN =		{urn:nbn:de:0030-drops-138837},
  doi =		{10.4230/LIPIcs.TYPES.2020.4},
  annote =	{Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.1
EasyCoding - Methodology to Support Programming Learning

Authors: Marcela Viana P. Almeida, Luís M. Alves, Maria João Varanda Pereira, and Glívia Angélica R. Barbosa

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
Knowing that the programming curricular units in the first year of engineering courses have a high failure rate and, assuming that this failure is due, in large part, to the lack of motivation and the lack of autonomy of the student to program in context outside the classroom, a methodology based on activity guides using attractive web platforms is proposed. The proposed methodology aims to facilitate both the planning of activities by the teachers and the autonomy and motivation by students. In order to receive a first feedback about this work, the methodology is being used by programming professors from Polytechnic Institute of Bragança, but in the near future it will be also evaluated by professors from the Federal Center of Technological Education of Minas Gerais and from the Federal Technological University of Paraná, both from Brazil. Following this work, a system is being developed that allows the automatic construction of guides based on exercises available from the web and systems that facilitate the collection of solutions and analysis of results.
Cite as

Marcela Viana P. Almeida, Luís M. Alves, Maria João Varanda Pereira, and Glívia Angélica R. Barbosa. EasyCoding - Methodology to Support Programming Learning. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 1:1-1:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almeida_et_al:OASIcs.ICPEC.2020.1,
  author =	{Almeida, Marcela Viana P. and Alves, Lu{\'\i}s M. and Pereira, Maria Jo\~{a}o Varanda and Barbosa, Gl{\'\i}via Ang\'{e}lica R.},
  title =	{{EasyCoding - Methodology to Support Programming Learning}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{1:1--1:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio 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.2020.1},
  URN =		{urn:nbn:de:0030-drops-122887},
  doi =		{10.4230/OASIcs.ICPEC.2020.1},
  annote =	{Keywords: learning programming, teaching programming, automatic activity guides, programming motivation}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.6
An Augmented Reality Mathematics Serious Game

Authors: José Manuel Cerqueira, João Martinho Moura, Cristina Sylla, and Luís Ferreira

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
This article presents the results obtained from an experiment using an Augmented Reality (AR) serious game for learning mathematical functions in middle school, in contexts that resort to Game Based Learning. A serious game was created specifically for this purpose and allowed to conduct an exploratory study with a quantitative and qualitative methodological approach, with two groups of teachers of different subjects: mathematics and informatics. The game, called FootMath, allows the visualization, manipulation and exploration of linear, quadratic, exponential and trigonometric mathematical functions, through the simulation of a 3D football game, in which the user can change the function parameters with different values, in order to score a goal. It was tested the potential use of AR technologies in learning scenarios, considering the teacher’s perspective. According to the findings, FootMath was considered to be a promising and innovative tool to be incorporated in real mathematics teaching scenarios.
Cite as

José Manuel Cerqueira, João Martinho Moura, Cristina Sylla, and Luís Ferreira. An Augmented Reality Mathematics Serious Game. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 6:1-6:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cerqueira_et_al:OASIcs.ICPEC.2020.6,
  author =	{Cerqueira, Jos\'{e} Manuel and Moura, Jo\~{a}o Martinho and Sylla, Cristina and Ferreira, Lu{\'\i}s},
  title =	{{An Augmented Reality Mathematics Serious Game}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{6:1--6:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio 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.2020.6},
  URN =		{urn:nbn:de:0030-drops-122939},
  doi =		{10.4230/OASIcs.ICPEC.2020.6},
  annote =	{Keywords: Serious Game, Augmented Reality, Mathematics, Functions}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.7
CodeCubes: Coding with Augmented Reality

Authors: Bárbara Cleto, Cristina Sylla, Luís Ferreira, and João Martinho Moura

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
CodeCubes is interface that uses Augmented Reality to stimulate Computational Thinking in young students. The visual programming blocks are replaced by paper cubes that have an Augmented Reality marker on each face. Each marker represents a programming instruction. The game is composed of three levels. It consists of programming a car course in a racetrack, driving from the start to the final goal. Code Cubes takes advantage of the physicality offered by Augmented Reality technology. We present the design and development of the game, focusing on its main characteristics and describing the various development stages. We also present the first results obtained by exploring Code Cubes. The results were positive, showing the potential of Augmented Reality interfaces in learning scenarios.
Cite as

Bárbara Cleto, Cristina Sylla, Luís Ferreira, and João Martinho Moura. CodeCubes: Coding with Augmented Reality. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 7:1-7:9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cleto_et_al:OASIcs.ICPEC.2020.7,
  author =	{Cleto, B\'{a}rbara and Sylla, Cristina and Ferreira, Lu{\'\i}s and Moura, Jo\~{a}o Martinho},
  title =	{{CodeCubes: Coding with Augmented Reality}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{7:1--7:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio 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.2020.7},
  URN =		{urn:nbn:de:0030-drops-122943},
  doi =		{10.4230/OASIcs.ICPEC.2020.7},
  annote =	{Keywords: Tangible Interfaces, Augmented Reality, Computational Thinking, Games}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2020.15
Learning Resources with Augmented Reality

Authors: Lázaro V. O. Lima, Cristiana Araújo, Luis Gonzaga Magalhães, and Pedro R. Henriques

Published in: OASIcs, Volume 81, First International Computer Programming Education Conference (ICPEC 2020)

Abstract
Preparing teachers and students for a connected and programmed world depends on how we develop and reinvent teaching tools. The society has realized and is absorbing Computational Thinking and its related skills. The pragmatics shows that a person only acquires a new way of thinking or a new way of behaving if he is trained with the appropriate devices. Computational Thinking should be training from an early age to acquire important skills; in that way, the interpretation and design of algorithms/programs will become much easier. However, the development of Computational Thinking requires the creation and use of appropriate Learning Resources (LR). We will discuss how an ontology can be used to specify what is involved in Computer Programming and how these concepts and Computational Thinking concepts are related. We believe that this formal description will guide the choice of convenient LR. In that context, we intend to investigate the impact of Augmented Reality on them. After presenting the ontological approach, the paper will focus on the process of shaping Computational Thinking through Augmented Reality. We aim at creating AR-based LR prototypes to validate the idea we present here. We are convinced that an attractive way to improve fundamental skills is necessary to practice and use these tools with young students, but LRs must be attractive, motivating and effective.
Cite as

Lázaro V. O. Lima, Cristiana Araújo, Luis Gonzaga Magalhães, and Pedro R. Henriques. Learning Resources with Augmented Reality. In First International Computer Programming Education Conference (ICPEC 2020). Open Access Series in Informatics (OASIcs), Volume 81, pp. 15:1-15:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lima_et_al:OASIcs.ICPEC.2020.15,
  author =	{Lima, L\'{a}zaro V. O. and Ara\'{u}jo, Cristiana and Magalh\~{a}es, Luis Gonzaga and Henriques, Pedro R.},
  title =	{{Learning Resources with Augmented Reality}},
  booktitle =	{First International Computer Programming Education Conference (ICPEC 2020)},
  pages =	{15:1--15:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-153-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{81},
  editor =	{Queir\'{o}s, Ricardo and Portela, Filipe and Pinto, M\'{a}rio 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.2020.15},
  URN =		{urn:nbn:de:0030-drops-123028},
  doi =		{10.4230/OASIcs.ICPEC.2020.15},
  annote =	{Keywords: Computational Thinking, Learning Resource, Augmented Reality, Teacher Support Tools}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2018
LIPIcs, Volume 130, TYPES'18, Complete Volume

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
LIPIcs, Volume 130, TYPES'18, Complete Volume
Cite as

Peter Dybjer, José Espírito Santo, and Luís Pinto. LIPIcs, Volume 130, TYPES'18, Complete Volume. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018,
  title =	{{LIPIcs, Volume 130, TYPES'18, Complete Volume}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018},
  URN =		{urn:nbn:de:0030-drops-114507},
  doi =		{10.4230/LIPIcs.TYPES.2018},
  annote =	{Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Peter Dybjer, José Espírito Santo, and Luís Pinto. Front Matter, Table of Contents, Preface, Conference Organization. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 0:i-0:x, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0,
  author =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0},
  URN =		{urn:nbn:de:0030-drops-114045},
  doi =		{10.4230/LIPIcs.TYPES.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.18
Modal Embeddings and Calling Paradigms

Authors: José Espírito Santo, Luís Pinto, and Tarmo Uustalu

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Gödel, of intuitionistic logic into IS4. As source system we take either the call-by-name (cbn) or the call-by-value (cbv) lambda-calculus with simple types. The target system can be taken to be the, arguably, simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. A slight refinement of the target and of the embeddings shows that: the target is a calculus indifferent to the calling paradigms cbn/cbv, obeying a new paradigm that we baptize call-by-box (cbb), and enjoying standardization; and that Girard’s (resp. Gödel’s) embbedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, using a compilation technique we call protecting-by-a-box, enjoying the preservation and reflection properties known for cps translations - but in a stronger form that allows the extraction of standardization for cbn or cbv as consequence of standardization for cbb. The modal target and embeddings achieve thus an unification of call-by-name and call-by-value as call-by-box.
Cite as

José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 18:1-18:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2019.18,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s and Uustalu, Tarmo},
  title =	{{Modal Embeddings and Calling Paradigms}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18},
  URN =		{urn:nbn:de:0030-drops-105256},
  doi =		{10.4230/LIPIcs.FSCD.2019.18},
  annote =	{Keywords: intuitionistic S4, call-by-name, call-by-value, comonadic lambda-calculus, standardization, indifference property}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.10
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts

Authors: José Espírito Santo, Maria João Frade, and Luís Pinto

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a lambda-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry-Howard interpretation (a kind of formal vector notation for lambda-terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs.
Cite as

José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 10:1-10:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2016.10,
  author =	{Esp{\'\i}rito Santo, Jos\'{e} and Frade, Maria Jo\~{a}o and Pinto, Lu{\'\i}s},
  title =	{{Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{10:1--10:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.10},
  URN =		{urn:nbn:de:0030-drops-98523},
  doi =		{10.4230/LIPIcs.TYPES.2016.10},
  annote =	{Keywords: sequent calculus, permutative conversion, Curry-Howard isomorphism, vector of arguments, generalized application, normal proof, natural proof, cut eli}
}
  • Refine by Author
  • 5 Espírito Santo, José
  • 5 Pinto, Luís
  • 2 Dybjer, Peter
  • 2 Ferreira, Luís
  • 2 Moura, João Martinho
  • Show More...

  • Refine by Classification
  • 4 Computing methodologies → Mixed / augmented reality
  • 3 Theory of computation → Type theory
  • 2 Applied computing → Interactive learning environments
  • 2 Computing methodologies → Natural language processing
  • 2 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 4 Augmented Reality
  • 3 Computational Thinking
  • 1 Archival Descriptions
  • 1 Awareness
  • 1 Capture-the-Flag
  • Show More...

  • Refine by Type
  • 15 document
  • 1 volume

  • Refine by Publication Year
  • 4 2019
  • 4 2020
  • 4 2021
  • 2 2023
  • 1 2010
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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