Search

Una de las cuestiones más debatidas en el campo de la enseñanza de las ciencias es la conexión entre el conocimiento generado por la investigación y la mejora de la práctica docente el aula. La presente aportación propone la utilización de un modelo para el diseño y la evaluación de enseñanza de las ciencias que pone énfasis en explicitar qué conocimientos se utilizan en el diseño y como se articulan en la toma de decisiones sobre aspectos específicos de la enseñanza de contenidos concretos. El objetivo principal es mejorar la comunicación de estos aspectos en el seno de la comunidad de investigadores. La aportación presenta la utilización de este modelo en dos tareas complementarias: el diseño de material didáctico para clases de ciencias en Inglaterra y la evaluación del uso de dicho material en el aula.

NASA’s Wide-Field Infrared Survey Telescope (WFIRST) is a space-based observatory currently under design and initial stages of fabrication, targeted to launch in the mid-2020s. The U.S. National Academy of Science’s Astro2010 decadal survey identified WFIRST as the highest-priority mission to investigate three fundamental problems in astronomy: the dark energy content of the Universe, the evolution of the high-redshift galaxy and quasar population, and the demographics of exoplanets in our own galaxy. Ball Aerospace is currently developing the mechanical/optical assembly for WFIRST’s key imager, the Wide Field Instrument. With its leading-edge mosaic of IR detectors, this imager will provide a field of view over 100 times greater than the competing instruments on the Hubble Space Telescope, thus opening an exciting new era in sky surveys from space. To achieve the mission’s ambitious science objectives, WFI must observe celestial objects over an exceptional range of brightness with extraordinary photometric precision. Ball Aerospace and Utah State University’s Space Dynamics Laboratory (SDL) are collaborating to design and build an onboard light source system capable of helping WFI meet these stringent photometric performance requirements. This Relative Calibration System (RCS) generates light matched to the wavelengths of each of the imager’s six filters, illuminating the WFI Focal Plane Assembly (FPA) with temporally stable illumination at six logarithmically-spaced signal levels. Measuring these light levels will define a detector response ratio we’ll use to define a transfer standard relating faint objects to bright ones. This talk will highlight the engineering methods we’ve employed to select the sources for use in the calibration system, some unexpected consequences of these choices, the lessons learned from the trade studies, and what challenges lie ahead in completing the RCS.

Hilbert's Foundations of Geometry was perhaps one of the most influential works of geometry in the 20th century and its axiomatics was the first systematic attempt to clear up the logical gaps of the Elements. But does it have gaps of its own? In this paper, we discuss a logical issue, asking how Hilbert is able to talk about natural numbers within a foundational synthetic geometry. We clarify the matter, showing how to obtain the natural numbers using a very modest subset of his axioms., 8 pages, 3 figures

NASA’s Wide-Field Infrared Survey Telescope (WFIRST) is a space-based observatory now being designed for launch in the mid-2020s. As the U.S. astronomical community’s top-priority mission for this decade, WFIRST is designed not only as a “discovery machine” for general PI-driven science but also as a survey platform to address three fundamental problems at the forefront of modern astrophysics: the dark energy content of the Universe, the evolution of the high-redshift galaxy and quasar population, and the demographics of exoplanets in our own galaxy. WFIRST’s primary camera, the Wide-Field Instrument (WFI), is a near-IR imager under development by Ball Aerospace and NASA’s Goddard Space Flight Center that will provide a field of view over 100 times greater than that of the Hubble Space Telescope. Achieving WFIRST’s key science objectives will require WFI to obtain imagery of faint galaxies, stars, and supernovae with unprecedented photometric precision. Attaining this level of accuracy demands calibrating the data at a level never previously accomplished in space. To meet these requirements, Ball Aerospace and Utah State University’s Space Dynamics Laboratory (SDL) are collaborating to design and build the Relative Calibration System (RCS) for WFI. The RCS is a self-calibrating unit which will generate temporally and spatially stable illumination of the WFI focal plane at a variety of wavelengths over an exceptionally large range of intensity. The RCS will enable not only standard tests of pixel-to-pixel sensitivity and gain from space, but also assessments of interpixel non-linearity, charge persistence, total-count-dependent non-linearity, and count-rate-dependent non-linearity throughout the mission’s lifetime. This talk will explore novel aspects of the RCS hardware design that permit the system to meet these demanding requirements.

We present a marriage of functional and structured imperative programming that embeds in pure lambda calculus. We describe how we implement the core of this language in a monadic DSL which is structurally equivalent to our intended source language and which, when evaluated, generates pure lambda terms in continuation-passing-style., 5 pages

We introduce a novel parsing concept called local lexing. It integrates the classically separated stages of lexing and parsing by allowing lexing to be dependent upon the parsing progress and by providing a simple mechanism for constraining lexical ambiguity. This makes it possible for language design to be composable not only at the level of context-free grammars, but also at the lexical level. It also makes it possible to include lightweight error-handling directly as part of the language specification instead of leaving it up to the implementation. We present a high-level algorithm for local lexing, which is an extension of Earley's algorithm. We have formally verified the correctness of our algorithm with respect to its local lexing semantics in Isabelle/HOL.

We introduce a novel parsing concept called local lexing. It integrates the classically separated stages of lexing and parsing by allowing lexing to be dependent upon the parsing progress and by providing a simple mechanism for constraining lexical ambiguity. This makes it possible for language design to be composable not only at the level of context-free grammars, but also at the lexical level. It also makes it possible to include lightweight error-handling directly as part of the language specification instead of leaving it up to the implementation. We present a high-level algorithm for local lexing, which is an extension of Earley's algorithm. We have formally verified the correctness of our algorithm with respect to its local lexing semantics in Isabelle/HOL.

The goal of the ProofPeer project is to make collaborative theorem proving a reality. An important part of our plan to make this happen is ProofScript, a language designed to be the main user interface of ProofPeer. Of foremost importance in the design of ProofScript is its fit within a collaborative theorem proving environment. By this we mean that it needs to fit into an environment where peers who are not necessarily part of the current theorem proving and programming language communities work independently from but collaboratively with each other to produce formal definitions and proofs. All aspects of ProofScript are shaped by this design principle. In this paper we will discuss ProofScript’s most important aspect of being an integrated language both for interactive proof and for proof scripting.

ZFH stands for Zermelo-Fraenkel set theory implemented in higher-order logic. It is a descendant of Agerholm’s and Gordon’s HOL- ST but does not allow the use of type variables nor the definition of new types. We first motivate why we are using ZFH for ProofPeer, the collaborative theorem proving system we are building. We then focus on the type inference algorithm we have developed for ZFH. In ZFH’s syntax, function application, written as juxtaposition, is overloaded to be either set-theoretic or higher-order. Our algorithm extends Hindley-Milner type inference to cope with this particular overloading of function application. We describe the algorithm, prove its correctness, and discuss why prior general approaches to type inference in the presence of coercions or over- loading do not cover our particular case.

The Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are five groups of axioms, each focused on a logical feature of Euclidean geometry. The first two groups give us ordered geometry, a highly limited setting where there is no talk of measure or angle. From these, we mechanically verify the Polygonal Jordan Curve Theorem, a result of much generality given the setting, and subtle enough to warrant a full verification. Along the way, we describe and implement a general-purpose algebraic language for proof search, which we use to automate arguments from the first axiom group. We then follow Hilbert through the preliminary definitions and theorems that lead up to his statement of the Polygonal Jordan Curve Theorem. These, once formalised and verified, give us a final piece of automation. Suitably armed, we can then tackle the main theorem.

We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems.

We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems.

Not Available

There is an extensive academic literature documenting students' pre-instructional interpretations of phenomena and events, showing that these interpretations are not consistent with 'energy' as used in physics. Furthermore, there is evidence showing that teaching does not always result in students' interpretations becoming consistent with teaching. This evidence has been collected across many decades and in many countries. This thesis presents a theoretical rationale for the design, implementation and evaluation of a teaching sequence aiming to promote conceptual understanding of the concept of energy to 15-16 years old physics students in Cyprus. Students' pre-instructional ideas about energy were investigated and were found to be consistent with those reported in the international literature. A design study was conducted with the aim of improving students' conceptual understanding compared to that might be expected from physics teaching usually conducted in Cyprus. Among the perspectives and the methods critically reviewed to inform the design, the perspective set out by Leach and Scott (2002) drawing on the concept of Learning Demand was chosen. Furthermore, the energy ideas proposed within the SPT11-14 project (2006) were used as a basis for the development of the theoretical framework of the teaching sequence.The research questions for the study were as follows: RQ1. What concepts of energy are used by a Cypriot cohort of upper high school students prior to teaching? RQ2. How do the conceptions and learning of the sub-cohort of Cypriot students taught through the research-informed approach compare with those following 'normal teaching' after instruction? RQ3. How do the understandings of the energy concept, of a small sub-group of students, develop during the lessons of the research-informed approach? The study involved thirty six Cypriot students in two classes of an urban upper secondary school. One of the classes acted as an intervention group, receiving the 'new' teaching sequence whilst the comparison group followed normal teaching. For addressing RQ1, data were collected through a pre-test administered to all participant students. Pre-test data and data collected through a post-test also administered to all participant students were used to test the comparative effectiveness of the teaching, thereby addressing RQ2. To address RQ3, data collected from a small number of experimental students through pre and post-test, two short-length diagnostic probes, two interviews and through an interview conducted with the experimental teacher were used.Analysis of data allowed for the following answers to each research question: RQ1: The students' pre-instructional views about the concept of energy were not within the current scientific beliefs; rather, these were within an alternative context. They were consistent with findings reported internationally in the literature. RQ2: The students' understandings of the concept of energy taught through the research-informed approach were significantly higher after instruction compared with those following 'normal teaching'. RQ3: The students' understandings of the concept of energy through the lessons of the research-informed approach were developed in a manner consistent with the intended aims of the teaching.The answers to the three research questions strongly suggest that the proposed teaching sequence for energy was found to be effective.