Skip.-0Page:%starting page number, <1 will be skipped later
Title:(Algebraic Typechecking for Stack Languages)
Paragraph:(Lorem ipsum dolor sit amet, consectetur adipiscing elit.
Donec egestas risus ipsum, et condimentum tellus varius id.
In pellentesque, mi et rutrum ultrices, neque nisl hendrerit ligula, et bibendum nulla risus a diam.)
Section:(Introduction)
% Paragraph: (Vestibulum volutpat maximus magna, ac imperdiet lorem efficitur in. Curabitur tortor felis, euismod vitae ipsum id, euismod condimentum libero. Aenean blandit lorem eu diam mattis tempor. Duis efficitur arcu id laoreet sollicitudin. Nam maximus id turpis sed sagittis. Proin nec sem eros. Proin at nisi ac dolor tincidunt suscipit. Proin eu aliquet tellus. Aenean tincidunt leo vel consectetur luctus. Morbi ac massa aliquet, lobortis metus non, venenatis mauris. Curabitur facilisis ultricies felis eu interdum.)
Paragraph:
(The work aims to explore a known, but underexplored way to think about typing stack languages.
Stack based Languages have seen a wide adoption as intermediate languages. Software written directly in them is relatively scarce.
Instead of thinking about typed programs in term of proofs, we will think about types as algebraic expressions.
Of course this algebra will be equivalent to some substructural logic, if you want to.)
Fin
Section:(1. Fundamentals)
Section:(1.1 What is a Stack Machine)
Paragraph:(When a function is evaluated, inputs and outputs aren't read from and written to registers.
Instead a function pops input values from a global stack and pushes a result back onto the same stack.
Allthough this simple architecture suffices to be Turing complete, many Stack oriented languages also allow one to define variables.
Another convinience are distinct stacks for distinct types of data. For example, FORTH uses a second stack to store floating point numbers, and PostScript uses a dictionary stack.
)
Force_New_Page.
%Example: 2 3 5 7 | 4 1 roll pop mul mul => 42
%2 3 5 7 on_stack execute 4 then 1 then /roll then /pop then /mul then /mull :End_Diagram