Abstract
We are assisting the rise of online coding environments as a strategy to promote youth tech employment. With the growing importance of the technology sector, these type of technical training programs give learners emergent tech skills with a big impact and relevance to the current professional market needs. In this realm, MOOCs (massive open online courses) and online coding bootcamps are two increasingly popular options for learners to improve their code development skills and find work within a relatively short amount of time. Among all the features available on these environments, one stands out, which is the code generation. This chapter aims to detail and compare the most popular solutions for both learning contexts based on several criteria such as impact and maturity, user groups, and tools and features. In the features field, the authors highlight the code generation feature as an efficient way to enhance exercise resolution.

Abstract
In this paper, we identify a subset of types in the rank 2 intersection type system, where types do not contain positive occurrences of intersections. We extend the notion of pre-grammar of a type and address the type-inhabitation problem for types in this subset, as well as their intersections.

Abstract

Abstract
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E , for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [19], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [19], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E , which can be seen as a refinement of system U , produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [19], which turn out to be an essential quantitative tool because they remove the confusion between âbeing a pairâ? and âbeing duplicableâ?. Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors. © LIPIcs 2020.

Abstract
The number of devices connected to the Internet has been increasing exponentially. There is a substantial amount of data being exchanged among numerous connected devices. The added convenience brought by these devices spans across multiple facets of everyday life, such as drivers reporting an accident through dash cams, patients monitoring their own health, and companies controlling the safety of their facilities. However, it is critical to increase safety and privacy across the data generated and propagated by these devices. Previous works have focused mainly on device management and relied on centralized solutions namely Public Key Infrastructure (PKI). This paper describes a novel mechanism that ensures secure autonomous communication between Internet of Things (IoT) devices, while using a completely decentralized solution that mitigates the classical single points-of-failure problem. This is accomplished by a new peer-to-peer protocol using Short Authentication Strings (SAS), in which verification is made through a Limited-Location Channel (LLC).

Abstract
There are many cryptographic protocols in the literature that are scientifically and mathematically sound. By extension, cryptography today seeks to respond to numerous properties of the communication process beyond confidentiality (secrecy), such as integrity, authenticity, and anonymity. In addition to the theoretical evidence, implementations must be equally secure. Due to the ever-increasing intrusion from governments and other groups, citizens are now seeking alternatives ways of communication that do not leak information. In this paper, we analyze multiparty computation (MPC), which is a sub-field of cryptography with the goal of creating methods for parties to jointly compute a function over their inputs while keeping those inputs private. This is a very useful method that can be used, for example, to carry out computations on anonymous data without having to leak that data. Thus, due to the importance of confidentiality in this type of technique, we analyze active and passive attacks using complexity measures (compression and entropy). We start by obtaining network traces and syscalls, then we analyze them using compression and entropy techniques. Finally, we cluster the traces and syscalls using standard clustering techniques. This approach does not need any deep specific knowledge of the implementations being analyzed. This paper presents a security analysis for four MPC frameworks, where three were identified as insecure. These insecure libraries leak information about the inputs provided by each party of the communication. Additionally, we have detected, through a careful analysis of its source code, that SPDZ-2's secret sharing schema always produces the same results.