Stochastically generating well-typed CPS-calculus terms : a context-directed algorithm.

Abstract

Continuações são frequentemente empregadas no contexto de compiladores, em especial como fundamento para representações intermediárias baseadas em continuation-passing style (CPS). Um campo emergente de pesquisa é o desenvolvimento de um cálculo baseado em CPS, visando-se criar uma base teórica para essas representações intermediárias. O trabalho atual tem o objetivo de contribuir a essa linha de pesquisa implementando uma variante de CPS-calculus em PLT Redex, formalizando um gerador de termos bem-tipados para essa linguagem e apresentando uma maneira de unir esses dois aspectos do trabalho em Racket, programando-se propriedades em Redex e depois testando-as usando o gerador de termos implementado em Rackcheck. Primeiramente, diversas semânticas de CPS-calculus foram implementadas, possibilitando o teste de reduções, tipagem e traduções entre CPS-calculus e λ-calculus, tanto por call-by-name quanto por call-by-value. Após, um gerador estocástico de termos bem-tipados foi formalizado usando-se árvores de provas e pseudo-código puramente funcional e depois implementado em Rackcheck, que possui suporte a shrinking automático de termos. Por último, foram testadas algumas propriedades sobre a imagem do gerador, além da propriedade de preservação de tipos da semântica operacional jump reduction e das traduções de λ-calculus para CPS-calculus. Com todos esses desenvolvimentos, o trabalho aqui apresentado obteve êxito em criar um caminho para possibilitar testes baseados em propriedades de CPS-calculus, algo que poderá ser de utilidade a futuras explorações acadêmicas no tópico, em especial como um prelúdio para provas formais que visa diminuir o tempo gasto com tentativas de se provar algo falso.