At the start of the millennium, the Cyclone language was developed as a solution to the memory safety shortcomings of the C language. Since then, many programming languages have emerged with their own memory safety strategies. But how can we validate those strategies? This paper proposes Porcelain: a semantic framework for representing and analyzing memory safety techniques. Introducing its definitions, use cases, and limitations whilst giving an overview of the current and future work.
Software Product Lines (SPLs) enable the systematic development of configurable software systems by organizing products as families that share commonalities and differ in selected features. However, static analysis in SPLs poses scalability challenges due to variability in space (across configurations) and variability in time (across software revisions). This paper presents an interpreter-based framework that combines variational lifting and memoization to support scalable and reusable static analysis of evolving SPLs. Analyses are implemented as PCF+ programs and executed over variational representations of object programs, annotated with presence conditions. Memoization mechanisms allow the reuse of previously computed results across object program evolutions, reducing redundant computations and contributing to performance improvements. The framework is evaluated using benchmarks simulating software evolution scenarios. Results indicate that the combined use of variational lifting and memoization effectively reduces execution time, suggesting the advantages of addressing both dimensions of variability. This work contributes a reusable infrastructure for control-flow-based analyses in SPLs and provides empirical evidence supporting its efficiency.
This paper presents a type-safe model of quantum computing, building upon the model introduced by Sabry in Haskell. By applying type-level programming techniques, we extend the model to constrain invalid operations and states at compile time. Our implementation enforces the no-cloning theorem at the type level via memory access patterns, while maintaining expressiveness via monadic composition of quantum operations. The implementation serves both as an introduction to quantum computing fundamentals and as a case study in enforcing physical constraints through a functional programming type system.
When using lambdas in managed languages, the programmer does not need to concern themselves with the disposal of the closure; in contrast, unmanaged languages that implement lambdas need mechanisms to make the closures be disposed safely at the right time. Through examples, we explore and compare the following languages: C++, Rust, and Swift. For each language, we implement examples of the usage of lambdas in increasing complexity, analyzing how they work while showcasing the implementations. After presenting the implementations, we contrast the languages regarding memory safety and typing. Finally, from those experiments, we assess some properties of lambdas in the languages and summarize them in a table, namely: safety features, safe by default, safety guarantees, verbosity, type flexibility, and memory overhead.
Kelsey demonstrou que a forma de atribuição estática única, comumente utilizada como uma linguagem intermediária para a implementação de otimizadores de código em compiladores de linguagens imperativas, pode ser caracterizada como uma linguagem funcional. Isso ocorre porque a mutabilidade local é eliminada por meio da criação de novas variáveis, e o fluxo de controle pode ser traduzido em abstrações lambda. A tradução dessa representação intermediária para a forma A-normal, frequentemente utilizada em compiladores para linguagens funcionais, é relativamente direta. Rigon et al. exploram essa característica, propondo um sistema que infere tipos e efeitos para uma linguagem com mecanismos de controle de fluxo similares aos de linguagens imperativas. Este trabalho expande essa proposta ao introduzir a tradução da representação intermediária na forma A-normal com efeitos algébricos para uma representação que lida com efeitos por meio de mônadas, onde a combinação de vários efeitos em uma mônada é representada por mônadas livres. Como resultado, é demonstrada a geração de código executável em linguagem Haskell, oferecendo indiretamente um meio simples para a definição de uma semântica para a forma de atribuição estática única.
