Photo of Ivan Perez

Ivan Perez

Email:

I am a software engineer, research scientist, and entrepreneur. I like Game Programming, GUIs, Multimedia, Reactivity and Functional Languages. I currently work for NIA as a senior research scientist contractor with NASA Langley Research Center. I am the founder of Keera Studios, the Haskell Game and Mobile App Programming Studio. In 2017, I finished my PhD, under the supervision of Henrik Nilsson and Graham Hutton.

Selected Publications

Runtime Verification and Validation of Functional Reactive Systems


Authors: Ivan Perez (NIA / NASA Formal Methods Group); Henrik Nilsson (University of Nottingham)
Journal of Functional Programming, 30, E28. 2020.
(official)
Many types of interactive applications, including reactive systems implemented in hardware, interactive physics simulations and games, raise particular challenges when it comes to testing and debugging. Reasons include de facto lack of reproducibility and difficulties of automatically generating suitable test data. This paper demonstrates that certain variants of functional reactive programming (FRP) implemented in pure functional languages can mitigate such difficulties by offering referential transparency at the level of whole programs. This opens up for a multi-pronged approach for assisting with testing and debugging that works across platforms, including assertions based on temporal logic, recording and replaying of runs (also from deployed code), and automated random testing using QuickCheck. When combined with extensible forms of FRP that allow for constrained side effects, it allows us to not only validate software simulations but to analyse the effect of faults in reactive systems, confirm the efficacy of fault tolerance mechanisms and perform software- and hardware-in-the-loop testing. The approach has been validated on non-trivial systems implemented in several existing FRP implementations, by means of careful debugging using a tool that allows the test or simulation under scrutiny to be controlled, moving along the execution time line, and pin-pointing of violations of assertions on personal computers as well as external devices.


Fault-tolerant functional reactive programming (extended version)


Authors: Ivan Perez (NIA / NASA Formal Methods Group); Alwyn Goodloe (NASA Langley Research Center)
Journal of Functional Programming, 30, E12. 2020.
(official)
Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation, and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and functional reactive programming (FRP) capture the essence of those languages in a way that is both elegant and robust. To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many functional reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults, and incorporating fault tolerance into FRP, requires a different construction and remains an open problem. This work demonstrates how to extend an existing functional reactive framework with fault tolerance features. At value level, we tag faulty signals with reliability and probability information and use random testing to inject faults and validate system properties encoded in temporal logic. At type level, we tag components with the kinds of faults they may exhibit and use type-level programming to obtain compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide system analysis and design, validate system properties in the presence of faults, perform runtime monitoring, and study the effects of different fault tolerance mechanisms.


Copilot 3


Authors: Ivan Perez (NIA / NASA Formal Methods Group); Frank Dedden (Netherlands Aerospace Center); Alwyn Goodloe (NASA Langley Research Center)
NASA Technical Memorandum NASA/TM-2020-220587. 2020.
(official)
Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. The introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. This paper presents Copilot 3, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware. This paper presents version 3 of the Copilot language, demonstrates its suitability with a number of examples, and discusses its use in larger applications. Additionally, it describes the framework?s architecture, its implementation as a Domain Specific Language (DSL) embedded in Haskell, and the progress of the project over the years.


Fault-Tolerant Swarms


Space Mission Challenges in Information Technology (SMC-IT) (Caltech, California, USA). 2019.
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Alwyn Goodloe (NASA Langley Research Center); William Edmonson (NCAT)
(official)(abstract)
Safety-critical systems must be engineered to be ultra-reliable. Redundancy is critical to tolerate faults that cannot be eliminated by using ruggedized or hardened computing. The use of small satellites allows new missions to be cost-effective, but it also introduces new problems in terms of robustness and fault handling. Apart from the inherent problems of working in a distributed setting, small sats normally lack the redundancy needed to deal with pernicious faults due to constraints on weight, cost and complexity. This paper presents and evaluates fault tolerance mechanisms in a swarm of satellites considered as a whole, making it robust to the failure of one or more satellites. The evaluation is performed with a computer model augmented with the properties desired from our system. We use a random testing tool to inject faults in different parts of our model and evaluate the fault detection and fault correction mechanisms we propose. Our results support the suitability of the proposed fault model, fault tolerant architecture, and evaluation methodology.


Formal Verification of System States for Spacecraft Automatic Maneuvering


AIAA SciTech Forum (2019-1187) (San Diego, California, USA). 2019.
Authors: Kerianne L. Hobbs (Air Force Research Laboratory); Ivan Perez (NIA / NASA Formal Methods Group); Aaron Fifarek (LinQuest Corporation); Eric M. Feron (Georgia Tech)
(official)(abstract)
As the complexity and number of space operations in Earth orbit continues to grow, there are increased opportunities to incorporate automatic or autonomous maneuvering as part of a space traffic management framework. Understanding the context of the automatic maneuver, including the conditions under which an automatic maneuver is acceptable, is important to the design of the overall automatic maneuver system. This work proposes and conducts formal verification of high-level system requirements to govern automatic maneuvering of satellites in the presence of safety interlocks or failures. Three examples of automatic maneuver contexts are considered: conjunction avoidance, especially in the presence of orbital debris; rendezvous and proximity operations, especially for service satellites and active debris removal; and station keeping, especially in large satellite constellations providing space-based services like Internet. The primary contribution of this paper is the development and analysis of formal requirements for high-level system states governing when an automatic maneuver is acceptable. The requirements serve as a baseline framework for future automatic spacecraft maneuver research.


Rhine: FRP with Type-Level Clocks


Haskell Symposium 2018 - Co-located with ICFP 2018 (St Louis, USA)
Authors: Manuel Bärenz and Ivan Perez
(official)(abstract)
Processing data at different rates is generally a hard problem in reactive programming. Buffering problems, lags, and concurrency issues often occur. Many of these problems are clock errors, where data at different rates is combined incorrectly. Techniques to avoid clock errors, such as type-level clocks and deterministic scheduling, exist in the field of synchronous programming, but are not implemented in general-purpose languages like Haskell. Rhine is a clock-safe library for synchronous and asynchronous Functional Reactive Programming (FRP). It separates the aspects of clocking, scheduling and resampling from each other, and ensures clock-safety at the type level. Concurrent communication is encapsulated safely. Diverse reactive subsystems can be combined in a coherent, declarative data-flow framework, while correct interoperability of data at different rates is guaranteed by type-level clocks. This provides a general-purpose framework that simplifies multi-rate FRP systems and can be used for game development, media applications, GUIs and embedded systems, through a flexible API with many reusable components.


Fault Tolerant Functional Reactive Programming


ICFP 2018 (St Louis, USA)
Authors: Ivan Perez
(official)(abstract)
Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and Functional Reactive Programming capture the essence of those languages in a way that is both elegant and robust. To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many Functional Reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults, and incorporating fault tolerance into Functional Reactive Programming, requires a different construction and remains an open problem. This work presents extensions to an existing functional reactive abstraction to facilitate tagging reactive transformations with hazard tags or confidence levels. We present a prototype framework to quantify the reliability of a reactive construction, by means of numeric factors or probability distributions, and demonstrate how to aid the design of fault-tolerant systems, by constraining the allowed reliability to required boundaries. By applying type-level programming, we show that it is possible to improve static analysis and have compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide their analysis and design, to test system properties, to verify fault tolerance properties, to perform runtime monitoring, to implement fault tolerance during execution and to address faults during runtime. We present implementations in Haskell and in Idris.


GALE: a functional Graphic Adventure Library and Engine


FARM 2017 - Colocated with ICFP 2017
Authors: Ivan Perez
(official)(abstract)
Functional Programming brings a promise of highly-declarative code, efficient, parallelisable execution, modularity and reusability. In spite of these advantages, the use of pure Functional Languages in commercial games is still rare. This is partially caused lack of backends for multimedia, lack of production tools, and the demon- stration that functional abstractions work for other than non-trivial examples. In this paper we present GALE, a Graphic Adventure Library and Engine implemented in Haskell. Our engine implements the basic common features available in similar commercial engines for graphic adventures. We show a high-level abstract definition of game descriptions that allows us not only to run them, but also to analyse them in compile time. We also demonstrate how this description allows us to provide novel features not available in traditional engines. Our system works on iOS, Android and desktop, and is accompanied by a development environment to compose the games with no prior programming skills.


Back to the Future: Time Travel in FRP


Haskell Symposium 2017 - Colocated with ICFP 2017
Authors: Ivan Perez
(official)(abstract)
Functional Reactive Programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and limiting the exploration of the past. In this paper we show how these constraints can be overcome, giving local control over the time domain, the direction of time and the sampling step. We study the behaviour of FRP expressions when time flows backwards, and demonstrate how to synchronize subsystems running asynchronously and at different sampling rates. We have verified the practicality of our approach with two non-trivial games in which time control is central to the gameplay.


Testing and Debugging Functional Reactive Programming


ICFP 2017 (Oxford, UK)
Authors: Ivan Perez and Henrik Nilsson
(official)(abstract)
Many types of interactive applications, including video games, raise particular challenges when it comes to testing and debugging. Reasons include de-facto lack of reproducibility and difficulties of automatically generating suitable test data. This paper demonstrates that certain variants of Functional Reactive Programming (FRP) implemented in pure functional languages can mitigate such difficulties by offering referential transparency at the level of whole programs. This opens up for a multi-pronged approach for assisting with testing and debugging that works across platforms, including assertions based on temporal logic, recording and replaying of runs (also from deployed code), and automated random testing using QuickCheck. The approach has been validated on real, non-trivial games implemented in the FRP system Yampa through a tool providing a convenient Graphical User Interface that allows the execution of the code under scrutiny to be controlled, moving along the execution time line, and pin-pointing of violations of assertions on PCs as well as mobile platforms.


Functional Reactive Programming, Refactored


Haskell Symposium 2016 - Colocated with ICFP 2016 (Nara, Japan)
Authors: Ivan Perez, Manuel Bärenz and Henrik Nilsson
(official) (abstract) (corrected submission) (implementation) (errata)
Functional Reactive Programming (FRP) has come to mean many things. Yet, scratch the surface of the multitude of realisations, and there is great commonality between them. This paper investigates this commonality, turning it into a mathematically coherent and practical FRP realisation that allows us to express the functionality of many existing FRP systems and beyond by providing a minimal FRP core parametrised on a monad. We give proofs for our theoretical claims and we have verified the practical side by benchmarking a set of existing, non-trivial Yampa applications running on top of our new system with very good results.


On the Mathematical Properties of Monadic Stream Functions (draft)


Authors: Manuel Bärenz, Ivan Perez, and Henrik Nilsson
(paper) (abstract)
Monadic Stream Functions are CPS functions parameterised over a monadic context. They form a suitable abstraction to describe reactive processes, but what properties do they fulfill? In this technical report we explore some of the properties of Monadic Stream Functions, in particular those related to Arrows and Causal Commutative Arrows.


Bridging the GUI Gap with Reactive Values and Relations


Haskell Symposium 2015 - Colocated with ICFP 2015 (Vancouver, Canada)
Authors: Ivan Perez and Henrik Nilsson
(official) (mirror) (abstract) (bibtex) (abstract)
Reactive Values are an abstraction for mutable elements with a change-propagation or notification mechanism. They enable abstract reactive programming by hiding details on how to access particular values, how to deal with concurrency, etc. They provide a uniform interface for GUI widget properties, application models (in MVC terminology), hardware, files, etc. Reactive Values can be connected to one another forming uni- or bi-directional Reactive Relations. For an implementation, see: Keera Hails


1st year PhD Report

University of Nottingham
(paper) (bibtex) (notes)
Includes an overview of GUI programming in Haskell and FRP, Reactive Values and Relations. Recommended for those who want to know more about the current state of FRP.


Declarative Game Programming: Distilled Tutorial


PPDP '14: International Symposium on Principles and Practice of Declarative Programming
Authors: Henrik Nilsson and Ivan Perez
(abstract) (bibtex) (exdended abstract)

Bridging the GUI Gap with Reactive Values and Relations (superceeded)

Trends in Functional Programming 2014 - The Netherlands
Authors: Ivan Perez and Henrik Nilsson
(paper) (bibtex)

Other Talks
  • Keynote: Streams, Reactivity and FRP: where we are, where to go. 6th Workshop on Reactive and Event-based Languages and Systems. Splash 2019. Athens, Greece. October 2019.
  • Introduction to Functional Programming. Netflix, Los Gatos, CA, USA. December 2018.
  • Functional Abstractions for Robust and Fault Tolerant Reactive Systems. Informal Sandwich Seminar Series at National Institute of Aerospace. May 2018.
  • Reactive Programming with Monadic Stream Functions. Informal Friday Lunch Meeting at NASA Langley Research Center Formal Methods Group. May 2018.
  • Keynote: Extensible Functional Reactive Programming Applied to iOS and Android Game Programming. Haskell in Leipzig. October 2017.
  • Our Tools for Mobile Haskell Games and Apps. At Haskell eXchange (as Keera Studios). October 2017.
  • Haskell Games and Apps for Android and iOS. At Commercial Users of Functional Programming (co-located with ICFP 2017, (as Keera Studios). September 2017.
  • Game Programming in Haskell - Baby steps. At University of Bamberg (as Keera Studios). February 2016.
  • Game Programming in Haskell. At Haskell eXchange (as Keera Studios). October 2015.
  • London Haskell Meetup Group. June 2015.
  • Game Programming made simple. At Technical University of Madrid. April 2015.
  • FP Days London (as Keera Studios). November 2014.
  • London Haskell Meetup Group. September 2014.
  • FPLAD 2014
  • University of Twente. March 2013.
  • Technical University of Madrid. December 2011.
Open Source Software

Dunai

(github)

A very fast, extensible reactive programming framework that supports Classic FRP, Arrowized FRP, Reactive Programming and Stream Programming.


Haskanoid

(github) (video)

A Haskell game that uses the wiimote and the kinect.


Keera Hails

(github)

A reactive programming framework that scales well for GUIs.


Yampa

(maintainer) (github)

A Functional Reactive Programming Domain-Specific Language.


Hcwiid

(maintainer) (github)

Haskell bindings for a library to access wiimotes on Linux.


Awards

Finalist and winner

Hacknotts - 2014

MLH Finalist and winner of the best project award (to call it something; it was the only non-sponsored prize) at Nottingham Hackathon, together with Manuel Bärenz. We created a custom keyboard on a breadboard with 11 buttons to control a Parrot Drone. The signal was processed by a Haskell Yampa program that sent out commands to the parrot via wifi. The drone was recognised by a separate Haskell game using Kinect and became the player of a sideways Flappy-bird-like Haskell game in which the sizes of the pipes were determined by IBM's stock prize over the last six years (gathered in runtime using Bloomberg's API). We later demonstrated this by playing Breakout with the same drone (using Haskell to control it).

Teaching

Teaching Assistant

University of Nottingham - UK
Other activities

Founder of Keera Studios

Founder of Keera Studios Ltd. (Facebook page), a game programming company that uses Functional Languages to deliver games for Android, iOS and desktop.

Education

PhD

University of Nottingham - UK

My major interest is Game Programming and User Interfaces in Functional Languages. My main supervisor was Henrik Nilsson and my second supervisor was Graham Hutton


Master's Degree in Computational Logic

Technical University of Madrid (Universidad Polit├ęcnica de Madrid - Spain)

Major: Functional and Logic Programming
Minor: Component-based architectures


Engineer in Computer Science*

Technical University of Madrid (Universidad Polit├ęcnica de Madrid - Spain)

Major: Functional Programming, Compilers
Minor: Security, Computer Vision
(*Universities in Spain did not use to follow the standard BSc system. An Engineering degree is five years of attending courses, plus a thesis, and legally equivalent under new rules to a BSc and an MSc. This degree is separate from my other Master's degree.)