A |

alpha-equivalence | Critical Pair Analysis in Nominal Rewriting |

arithmetization | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |

automated reasoning | Determining automatically compass and straightedge unconstructibility in triangles |

B |

binding-time analysis | Automatic Staging via Partial Evaluation Techniques |

bit-size | Bit-size reduction of triangular sets in two and three variables |

C |

Compass and straightedge construction | Determining automatically compass and straightedge unconstructibility in triangles |

completeness | A rewrite-based computational model for functional logic programming |

component-based software engineering | Expression Compatibility Problem |

computational origami | A Mathematica module for Conformal Geometric Algebra and Origami Folding |

confluence | Critical Pair Analysis in Nominal Rewriting |

Conformal Geometric Algebra | A Mathematica module for Conformal Geometric Algebra and Origami Folding |

congruence closure | A Data Structure to Handle Large Sets of Equal Terms |

Coq | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry Verification of a brick Wang tiling algorithm Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |

critical pairs | Critical Pair Analysis in Nominal Rewriting |

cross-stage persistence | Automatic Staging via Partial Evaluation Techniques |

D |

data structure | A Data Structure to Handle Large Sets of Equal Terms |

decision procedure | A Data Structure to Handle Large Sets of Equal Terms |

delimited continuations | Implementing a stepper using delimited continuations |

E |

Expression Compatibility Problem | Expression Compatibility Problem |

expression problem | Expression Compatibility Problem |

expression simplification | A Data Structure to Handle Large Sets of Equal Terms |

F |

formal semantics | Expression Compatibility Problem |

formalization | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |

formalized mathematics | Compass-free Navigation of Mazes |

functional logic programming | A rewrite-based computational model for functional logic programming |

G |

geometry | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry Compass-free Navigation of Mazes |

I |

interactive theorem proving | Compass-free Navigation of Mazes |

L |

Lagrange interpolation | Bit-size reduction of triangular sets in two and three variables |

lexicographic Groebner bases | Bit-size reduction of triangular sets in two and three variables |

Lightweight Family Polymorphism | Expression Compatibility Problem |

M |

Mathematica | A Mathematica module for Conformal Geometric Algebra and Origami Folding |

multiplicity | Bit-size reduction of triangular sets in two and three variables |

N |

narrowing | A rewrite-based computational model for functional logic programming |

network monitors | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |

Nominal rewriting | Critical Pair Analysis in Nominal Rewriting |

P |

partial evaluation | Automatic Staging via Partial Evaluation Techniques |

planarity | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |

PLCA | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |

predicate logic | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |

program verification | Verification of a brick Wang tiling algorithm |

proof assistant | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |

Q |

qualitative spatial reasoning | Towards Verified Construction for Planar Class of a Qualitative Spatial Representation |

S |

shift and reset | Implementing a stepper using delimited continuations |

soundness | A rewrite-based computational model for functional logic programming |

space complexity | Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors |

staging | Automatic Staging via Partial Evaluation Techniques |

stepper | Implementing a stepper using delimited continuations |

strategies | A rewrite-based computational model for functional logic programming |

symbolic computation | Determining automatically compass and straightedge unconstructibility in triangles |

T |

Tarski's system of geometry | From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry |

term equivalence | A Data Structure to Handle Large Sets of Equal Terms |

theory of equality | A Data Structure to Handle Large Sets of Equal Terms |

Triangular Sets | Bit-size reduction of triangular sets in two and three variables |

W |

Wang tiling | Verification of a brick Wang tiling algorithm |