-
First Steps towards K-12 Computer Science Education in Portugal -- Experience Report
Authors:
Fernando Luis Neves,
Jose Nuno Oliveira
Abstract:
Computer scientists Jeannette Wing and Simon Peyton Jones have catalyzed a pivotal discussion on the need to introduce computing in K-12 mandatory education. In Wing's own words, computing 'represents a universally applicable attitude and skill set everyone, not just computer scientists, would be eager to learn and use.'' The crux of this educational endeavor lies in its execution. This paper repo…
▽ More
Computer scientists Jeannette Wing and Simon Peyton Jones have catalyzed a pivotal discussion on the need to introduce computing in K-12 mandatory education. In Wing's own words, computing 'represents a universally applicable attitude and skill set everyone, not just computer scientists, would be eager to learn and use.'' The crux of this educational endeavor lies in its execution. This paper reports on the efforts of the ENSICO association to implement such aims in Portugal. Starting with pilot projects in a few schools in 2020, it is currently working with 4500 students, 35 schools and 100 school teachers. The main aim is to gain enough experience and knowledge to eventually define a comprehensive syllabus for teaching computing as a mandatory subject throughout the basic and secondary levels of the Portuguese educational system. A structured framework for integrating computational thinking into K-12 education is proposed, with a particular emphasis on mathematical modeling and the functional programming paradigm. This approach is chosen for its potential to promote analytical and problem-solving skills of computational thinking aligned with the core background on maths and science.
△ Less
Submitted 15 November, 2024;
originally announced November 2024.
-
Compiling quantamorphisms for the IBM Q Experience
Authors:
Ana Neri,
Rui Soares Barbosa,
José N. Oliveira
Abstract:
Based on the connection between the categorical derivation of classical programs from specifications and the category-theoretic approach to quantum physics, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available at the IBM Q Experience.…
▽ More
Based on the connection between the categorical derivation of classical programs from specifications and the category-theoretic approach to quantum physics, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available at the IBM Q Experience. Quantum circuit reversibility is ensured by minimal complements, extended recursively. Measurements are postponed to the end of such recursive computations, termed "quantamorphisms", thus maximising the quantum effect. Quantamorphisms are classical catamorphisms which, extended to ensure quantum reversibility, implement quantum cycles (vulg. for-loops) and quantum folds on lists. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper to the Qiskit interface to IBM Q quantum devices. The generated quantum circuits - often quite large - exhibit the predicted behaviour. However, running them on real quantum devices incurs into a significant amount of errors. As quantum devices are constantly evolving, an increase in reliability is likely in the near future, allowing for our programs to run more accurately.
△ Less
Submitted 21 October, 2020;
originally announced October 2020.
-
The Home Office in Times of COVID-19 Pandemic and its impact in the Labor Supply
Authors:
José Nilmar Alves de Oliveira,
Jaime Orrillo,
Franklin Gamboa
Abstract:
We lightly modify Eriksson's (1996) model to accommodate the home office in a simple model of endogenous growth. By home office we mean any working activity carried out away from the workplace which is assumed to be fixed. Due to the strong mobility restrictions imposed on citizens during the COVID-19 pandemic, we allow the home office to be located at home. At the home office, however, in consequ…
▽ More
We lightly modify Eriksson's (1996) model to accommodate the home office in a simple model of endogenous growth. By home office we mean any working activity carried out away from the workplace which is assumed to be fixed. Due to the strong mobility restrictions imposed on citizens during the COVID-19 pandemic, we allow the home office to be located at home. At the home office, however, in consequence of the fear and anxiety workers feel because of COVID-19, they become distracted and spend less time working. We show that in the long run, the intertemporal elasticity of substitution of the home-office labor is sufficiently small only if the intertemporal elasticity of substitution of the time spent on distracting activities is small enough also.
△ Less
Submitted 8 July, 2020; v1 submitted 4 July, 2020;
originally announced July 2020.
-
Typed Linear Algebra for Efficient Analytical Querying
Authors:
João M. Afonso,
Gabriel D. Fernandes,
João P. Fernandes,
Filipe Oliveira,
Bruno M. Ribeiro,
Rogério Pontes,
José N. Oliveira,
Alberto J. Proença
Abstract:
This paper uses typed linear algebra (LA) to represent data and perform analytical querying in a single, unified framework. The typed approach offers strong type checking (as in modern programming languages) and a diagrammatic way of expressing queries (paths in LA diagrams). A kernel of LA operators has been implemented so that paths extracted from LA diagrams can be executed. The approach is val…
▽ More
This paper uses typed linear algebra (LA) to represent data and perform analytical querying in a single, unified framework. The typed approach offers strong type checking (as in modern programming languages) and a diagrammatic way of expressing queries (paths in LA diagrams). A kernel of LA operators has been implemented so that paths extracted from LA diagrams can be executed. The approach is validated and evaluated taking TPC-H benchmark queries as reference. The performance of the LA-based approach is compared with popular database competitors (PostgreSQL and MySQL).
△ Less
Submitted 3 September, 2018;
originally announced September 2018.
-
Programming from Metaphorisms
Authors:
J. N. Oliveira
Abstract:
This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism ref…
▽ More
This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.
△ Less
Submitted 19 September, 2017;
originally announced September 2017.
-
Typing linear algebra: A biproduct-oriented approach
Authors:
Hugo Daniel Macedo,
José N. Oliveira
Abstract:
Interested in formalizing the generation of fast running code for linear algebra applications, the authors show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of prog…
▽ More
Interested in formalizing the generation of fast running code for linear algebra applications, the authors show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biproduct equations makes it easy to calculate algorithms implementing matrix multiplication, the central operation of matrix algebra, ranging from its divide-and-conquer version to its vectorization implementation. From errant attempts to learn how particular products and coproducts emerge from biproducts, not only blocked matrix algebra is rediscovered but also a way of extending other operations (e.g. Gaussian elimination) blockwise, in a calculational style, is found. The prospect of building biproduct-based type checkers for computer algebra systems such as MatlabTM is also considered.
△ Less
Submitted 17 December, 2013;
originally announced December 2013.
-
Calculating risk in functional programming
Authors:
Daniel Murta,
Jose Nuno Oliveira
Abstract:
In the trend towards tolerating hardware unreliability, accuracy is exchanged for cost savings. Running on less reliable machines, "functionally correct" code becomes risky and one needs to know how risk propagates so as to mitigate it. Risk estimation, however, seems to live outside the average programmer's technical competence and core practice. In this paper we propose that risk be constructive…
▽ More
In the trend towards tolerating hardware unreliability, accuracy is exchanged for cost savings. Running on less reliable machines, "functionally correct" code becomes risky and one needs to know how risk propagates so as to mitigate it. Risk estimation, however, seems to live outside the average programmer's technical competence and core practice. In this paper we propose that risk be constructively handled in functional programming by (a) writing programs which may choose between expected and faulty behaviour, and by (b) reasoning about them in a linear algebra extension to standard, a la Bird-Moor algebra of programming. In particular, the propagation of faults across standard program transformation techniques known as tupling and fusion is calculated, enabling the fault of the whole to be expressed in terms of the faults of its parts.
△ Less
Submitted 14 November, 2013;
originally announced November 2013.
-
Functions as types or the "Hoare logic" of functional dependencies
Authors:
Jose N. Oliveira
Abstract:
Inspired by the trend on unifying theories of programming, this paper shows how the algebraic treatment of standard data dependency theory equips relational data with functional types and an associated type system which is useful for type checking database operations and for query optimization.
Such a typed approach to database programming is then shown to be of the same family as other programm…
▽ More
Inspired by the trend on unifying theories of programming, this paper shows how the algebraic treatment of standard data dependency theory equips relational data with functional types and an associated type system which is useful for type checking database operations and for query optimization.
Such a typed approach to database programming is then shown to be of the same family as other programming logics such as eg. Hoare logic or that of strongest invariant functions which has been used in the analysis of while statements.
The prospect of using automated deduction systems such as Prover9 for type-checking and query optimization on top of such an algebraic approach is considered.
△ Less
Submitted 17 October, 2012;
originally announced October 2012.
